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...

1 files changed, 4 insertions, 4 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
+}