summaryrefslogtreecommitdiff
path: root/src/editor/simple/editor.css
diff options
context:
space:
mode:
authorhallgren <hallgren@chalmers.se>2011-06-08 15:29:50 +0000
committerhallgren <hallgren@chalmers.se>2011-06-08 15:29:50 +0000
commit25ae9b2dc4d2a2a5bd2e1920e1ee82dfbef4162e (patch)
treedda562ccde336a8a624a19f7aae42a4f4705f30e /src/editor/simple/editor.css
parent25a9efb13c05bc806dff8d23c6be97013aa981ea (diff)
gfse: initial support for grammars in the cloud
This lets the user access the same set of grammars from multiple devices. Sharing grammars between multiple users is possible but discouraged at the moment. There is no version handling, so concurrent editing of the same grammar by different users might result in one user overwriting changes made by another user. (The same goes for cuncurrent editing on multiple devices by a single user, of course.)
Diffstat (limited to 'src/editor/simple/editor.css')
-rw-r--r--src/editor/simple/editor.css11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/editor/simple/editor.css b/src/editor/simple/editor.css
index 7bce43c3f..32625e699 100644
--- a/src/editor/simple/editor.css
+++ b/src/editor/simple/editor.css
@@ -4,7 +4,8 @@ h1,h2,h3,h4,small { font-family: sans-serif; }
h1:first-child, h2:first-child { margin-top: 0; margin-bottom: 1ex; }
#editor { max-width: 50em; }
-div.grammar { border: 1px solid black; background: #9df; }
+div.home, div.grammar { border: 1px solid black; background: #9df; }
+div.home { padding: 5px; }
div.files { margin: 0 8px 8px 8px; }
div#file { border: 2px solid #009; border-top-width: 0; }
@@ -13,12 +14,12 @@ div#file, pre.plain { background: white; padding: 0.6ex; }
.slideshow .hidden { display: none; }
-img.right, div.right, div.modtime { float: right; }
+img.cloud, img.right, div.right, div.modtime { float: right; }
.modtime { color: #999; white-space: nowrap; }
div.namebar { background: #9df; }
div.namebar table { width: 100%; }
-.namebar h3 { margin: 0; color: #009; }
+.namebar h3, .home h3 { margin: 0; color: #009; }
td.right { text-align: right; }
@@ -74,4 +75,6 @@ table.tabs input[type=button] {
/*text-decoration: underline;*/
}
-input.string_edit { font-family: inherit; font-size: inherit; } \ No newline at end of file
+input.string_edit { font-family: inherit; font-size: inherit; }
+
+ul.languages { -moz-column-width: 20em; }