diff options
Diffstat (limited to 'src/www/minibar')
| -rw-r--r-- | src/www/minibar/minibar.css | 13 | ||||
| -rw-r--r-- | src/www/minibar/minibar.js | 4 |
2 files changed, 12 insertions, 5 deletions
diff --git a/src/www/minibar/minibar.css b/src/www/minibar/minibar.css index d68784d51..cbfc04638 100644 --- a/src/www/minibar/minibar.css +++ b/src/www/minibar/minibar.css @@ -5,8 +5,12 @@ body.minibar { h1, h2, h3, small, th { font-family: sans-serif; } h1, h2, h3 { color: #303030; text-shadow: rgba(0,0,0,0.25) 3px 3px 5px; } +h1:first-child, h2:first-child { margin-top: 0; margin-bottom: 1ex; } + th, td { vertical-align: baseline; text-align: left; } +div.menubar { font-family: sans-serif; font-size: small; } + div#surface { min-height: 3ex; margin: 5px; @@ -67,10 +71,13 @@ div.brackets { span.brackets { background: #ddd; display: inline-block; - border: 1px solid black; - padding: 3px; + border-color: black; + border-style: solid; + border-width: 0 0 1px 0; + /*border: 1px solid black;*/ + padding: 2px 3px; } div.brackets .token { - padding: 0.5ex + padding: 0 0.5ex; } diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js index 466886865..10a469b6b 100644 --- a/src/www/minibar/minibar.js +++ b/src/www/minibar/minibar.js @@ -45,7 +45,7 @@ function Minibar(server,opts) { /* --- Creating user interface elements --------------------------------- */ - this.menubar=empty("div"); + this.menubar=div_class("menubar"); this.extra=div_id("extra"); this.minibar=element(this.options.target); @@ -94,7 +94,7 @@ Minibar.prototype.show_grammarlist=function(dir,grammar_names,dir_count) { function pick_first_grammar() { if(t.timeout) clearTimeout(t.timeout),t.timeout=null; if(t.grammar_menu.length>1 && !t.grammar_menu.parentElement) { - t.grammar_menu.onchange=bind(pick,t); + t.grammar_menu.onchange=pick; insertFirst(t.menubar,button("i",bind(t.show_grammarinfo,t))) insertFirst(t.menubar,t.grammar_menu); insertFirst(t.menubar,text("Grammar: ")); |