diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css index fa5d21306..c6973f2d5 100644 --- a/src/www/gfse/editor.css +++ b/src/www/gfse/editor.css @@ -129,7 +129,7 @@ textarea.text_mode { width: 99%; } -div#minibar { +div#minibar, div#syntax_editor { border: 1px solid black; padding: 5px; background: #ccc url("../minibar/brushed-metal.png"); diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js index f3f5bf98f..11ba18b37 100644 --- a/src/www/gfse/editor.js +++ b/src/www/gfse/editor.js @@ -370,6 +370,7 @@ function compile_button(g,err_ind) { function minibar_button(g,files,err_ind,comp_btn) { var b2; var minibar_div=div_id("minibar"); + var editor_div= div_id("syntax_editor"); function page_overlay(inner) { return wrap_class("table","page_overlay",tr(td(inner))) @@ -530,7 +531,7 @@ function minibar_button(g,files,err_ind,comp_btn) { function goto_minibar() { clear(files); - files.appendChild(minibar_div); + appendChildren(files,[minibar_div,editor_div]); var online_options={grammars_url: local.get("dir")+"/", grammar_list: [g.basename+".pgf"]} var pgf_server=pgf_online(online_options) diff --git a/src/www/gfse/index.html b/src/www/gfse/index.html index cfa89762d..12f50ef7e 100644 --- a/src/www/gfse/index.html +++ b/src/www/gfse/index.html @@ -33,23 +33,25 @@ This page does not work without JavaScript.