diff options
| author | hallgren <hallgren@chalmers.se> | 2011-06-08 15:29:50 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2011-06-08 15:29:50 +0000 |
| commit | 25ae9b2dc4d2a2a5bd2e1920e1ee82dfbef4162e (patch) | |
| tree | dda562ccde336a8a624a19f7aae42a4f4705f30e /src/editor/simple/editor.css | |
| parent | 25a9efb13c05bc806dff8d23c6be97013aa981ea (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.css | 11 |
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; } |
