From 4ddf81c05f2c3c67b4443d09d646b8a7bf973dfa Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Thu, 5 Apr 2012 15:25:10 +0000
Subject: [PATCH] minibar&gfse: grammar extension user interface fixes

It works OK now, but it could be better, e.g. the number of mouse clicks
required to enter an extension could to be reduced...
---
 src/www/gfse/editor.css |  8 ++++----
 src/www/gfse/editor.js  | 36 +++++++++++++++++++++++-------------
 2 files changed, 27 insertions(+), 17 deletions(-)

diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css
index 9dd9a091f..b2347cb44 100644
--- a/src/www/gfse/editor.css
+++ b/src/www/gfse/editor.css
@@ -15,9 +15,9 @@ h1:first-child, h2:first-child { margin-top: 0; margin-bottom: 1ex; }
 
 div.home, div.grammar { border: 1px solid black; background: #9df; }
 div.home { padding: 5px; }
-div.files { margin: 0 8px 8px 8px; }
+div.files { margin: 0 8px 8px 8px; position: relative; }
 
-div#file, table.extension td, table.extension th { border: 2px solid #009 }
+div#file, table.extension td, table.extension th { border: 2px solid #009; }
 div#file { border-top-width: 0; }
 pre.plain { border: 2px solid #009; }
 div#file, pre.plain { background: white; padding: 0.6ex; }
@@ -25,7 +25,7 @@ div#file, pre.plain { background: white; padding: 0.6ex; }
 table.extension { border-collapse: collapse; background: white; }
 table.extension td, table.extension th { padding: 1ex; }
 table.extension th { border-right-width: 0; color: #009; }
-table.extension td { border-left-width: 0; }
+table.extension td { border-left-width: 0; min-width: 30em; }
 
 .slideshow .hidden { display: none; }
 
@@ -133,4 +133,4 @@ div.grammar_extension {
     padding: 2ex;
     margin: 2ex;
     box-shadow: 10px 10px 10px rgba(0,0,0,0.3);
-}
\ No newline at end of file
+}
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js
index 8c8c0f31f..a4878c9db 100644
--- a/src/www/gfse/editor.js
+++ b/src/www/gfse/editor.js
@@ -146,14 +146,14 @@ function draw_grammar(g) {
 
 function draw_namebar(g,files) {
     var err_ind=empty("small"); // space for error indicator
+    var cb=compile_button(g,err_ind);
+    var mb=minibar_button(g,files,err_ind,cb);
+    var qb=quiz_button(g,err_ind);
+    //var pb=draw_plainbutton(g,files);
+    var xb=draw_closebutton(g);
     return div_class("namebar",
-		  [table([tr([td(draw_name(g)),
-			      td_right([err_ind,
-					compile_button(g,err_ind),
-					minibar_button(g,files,err_ind),
-					quiz_button(g,err_ind),
-					/*draw_plainbutton(g,files),*/
-					draw_closebutton(g)])])])])
+		     [table([tr([td(draw_name(g)),
+				 td_right([err_ind,cb,mb,qb/*,pb*/,xb])])])])
 }
 
 function draw_name(g) {
@@ -219,8 +219,9 @@ function compile_button(g,err_ind) {
     return b;
 }
 
-function minibar_button(g,files,err_ind) {
+function minibar_button(g,files,err_ind,comp_btn) {
     var b2;
+    var minibar_div=div_id("minibar");
 
     function page_overlay(inner) {
 	return wrap_class("table","page_overlay",tr(td(inner)))
@@ -300,7 +301,8 @@ function minibar_button(g,files,err_ind) {
 		if(res.errorcode=="OK") {
 		    extend_grammar(g);
 		    save_grammar(g);
-		    document.body.removeChild(overlay)
+		    files.removeChild(overlay)
+		    minibar_div.style.minHeight="0px";
 		    if(update_minibar) update_minibar();
 		    //goto_minibar();
 		}
@@ -311,18 +313,25 @@ function minibar_button(g,files,err_ind) {
 	    compile_grammar(newg,err_ind,save_if_ok);
 	}
 	function cancel_extension() {
-	    document.body.removeChild(overlay)
+	    files.removeChild(overlay)
+	    minibar_div.style.minHeight="0px";
 	    //goto_minibar();
 	}
-	document.body.appendChild(overlay)
 	draw_extension();
+	files.appendChild(overlay)
+	// Hack to prevent the overlay from overflowing the minibar div:
+	minibar_div.style.minHeight=overlay.clientHeight-11+"px"
+	//overlay.onresize= ... // doesn't work :-(
     }
 
-    function show_editor() { edit_grammar(g); }
+    function show_editor() {
+	clear(minibar_div);
+	edit_grammar(g);
+    }
 
     function goto_minibar() {
 	clear(files);
-	files.appendChild(div_id("minibar"));
+	files.appendChild(minibar_div);
 	var online_options={grammars_url: local.get("dir")+"/",
 			    grammar_list: [g.basename+".pgf"]}
 	var pgf_server=pgf_online(online_options)
@@ -338,6 +347,7 @@ function minibar_button(g,files,err_ind) {
 	}
 	var minibar=new Minibar(pgf_server,minibar_options);
 	b.style.display="none";
+	comp_btn.disabled=true;
 	if(b2) b2.style.display="";
 	else {
 	    b2=button("Show editor",show_editor);