mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
25ae9b2dc4
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.)
81 lines
2.3 KiB
CSS
81 lines
2.3 KiB
CSS
body { background: #eee; }
|
|
h1 { font-size: 175%; }
|
|
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.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; }
|
|
pre.plain { border: 2px solid #009; }
|
|
div#file, pre.plain { background: white; padding: 0.6ex; }
|
|
|
|
.slideshow .hidden { display: none; }
|
|
|
|
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, .home h3 { margin: 0; color: #009; }
|
|
|
|
td.right { text-align: right; }
|
|
|
|
.kw { font-weight: bold; font-family: sans-serif; color: #009; }
|
|
.sep { font-weight: bold; color: #009; }
|
|
|
|
div.indent { padding-left: 1em; min-width: 1em; min-height: 1em; }
|
|
|
|
/*
|
|
div.fun, div.param, div.lincat, div.oper, div.lin
|
|
{ padding-left: 2em; text-indent: -2em; }
|
|
*/
|
|
.more, .delete { font-weight: bold; font-family: sans-serif; }
|
|
.more, .delete, .edit { cursor: pointer; }
|
|
|
|
.hover .more, .hover .delete, .hover .edit { visibility: hidden }
|
|
|
|
.hover .hidden, .nohover .ifhover { display: none; }
|
|
|
|
.editable:hover, .deletable:hover { background: #ff9; }
|
|
|
|
.extensible:hover .more,.editable:hover > .edit ,.deletable:hover > .delete
|
|
{ visibility: visible; }
|
|
|
|
.more { color: green; }
|
|
.edit { color: orange; }
|
|
.delete { color: red; }
|
|
.error_message,.inError { color: red; }
|
|
.template, .template .sep { color: #999; }
|
|
form { display: inline-block; }
|
|
|
|
table.tabs {
|
|
width: 100%;
|
|
border-width: 0; border-spacing: 0; empty-cells: show;
|
|
}
|
|
|
|
table.tabs td { text-align: center; border: 2px solid #009; padding: 2px; }
|
|
table.tabs td.active { background: white; border-bottom-width: 0; }
|
|
table.tabs td.inactive {
|
|
background: #cef;
|
|
border-top-color: #66c; border-left-color: #66c; border-right-color: #66c;
|
|
}
|
|
|
|
table.tabs td.gap
|
|
{ border-top-width: 0; border-left-width: 0; border-right-width: 0; }
|
|
|
|
table.tabs input[type=button] {
|
|
border: 0;
|
|
background: inherit;
|
|
color: #009;
|
|
font-size: inherit;
|
|
font-weight: bold;
|
|
/*text-decoration: underline;*/
|
|
}
|
|
|
|
input.string_edit { font-family: inherit; font-size: inherit; }
|
|
|
|
ul.languages { -moz-column-width: 20em; }
|