minibar & cloud service: minor style changes

Also include the GF logo on the cloud service start page.

4 files changed, 14 insertions, 6 deletions

diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css
index b2347cb44..ff5554175 100644
--- a/src/www/gfse/editor.css
+++ b/src/www/gfse/editor.css
@@ -4,6 +4,7 @@ h1,h2,h3,h4,small { font-family: sans-serif;}
 h1,h2,h3,h4 { 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; }
+h1 img { float: right; border: 0; max-width: 50%; }
 
 #editor {
     /* This allows the div to grow wider than the window if necessary to
diff --git a/src/www/index.html b/src/www/index.html
index 440235e1f..499f4be37 100644
--- a/src/www/index.html
+++ b/src/www/index.html
@@ -7,7 +7,7 @@
 <link rel="stylesheet" type="text/css" href="gfse/editor.css" title="Cloud">
 <meta name = "viewport" content = "width = device-width">
 
-<h1>GF Cloud Service</h1>
+<h1><a href="http://www.grammaticalframework.org/"><img src="Logos/gf0.png" alt=""></a>GF Cloud Service</h1>
 
 <h2>Available Web Applications</h2>
 
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: "));