diff options
Diffstat (limited to 'src/www/syntax-editor/editor.css')
| -rw-r--r-- | src/www/syntax-editor/editor.css | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/www/syntax-editor/editor.css b/src/www/syntax-editor/editor.css index f3dd244d4..d1964c306 100644 --- a/src/www/syntax-editor/editor.css +++ b/src/www/syntax-editor/editor.css @@ -3,12 +3,12 @@ body.syntax-editor { } .hidden -{ +{ display:none; } .editor select#to_menu -{ +{ height: 10em; position: absolute; min-width: 5em; @@ -35,7 +35,7 @@ body.syntax-editor { padding: 0.2em; } -#tree +#tree, #tree_str { white-space:pre; font-family: monospace; @@ -57,18 +57,24 @@ body.syntax-editor { } #tree .node a -{ +{ cursor: pointer; } #tree .node a:hover -{ +{ text-decoration: underline; } #tree .node a.current -{ +{ font-weight: bold; } +#tree_str +{ + font-size:0.85em; + color:#666; + } + #refinements { /* display: inline-block; */ @@ -99,7 +105,7 @@ body.syntax-editor { } .refinement -{ +{ margin: 0.1em; display: inline-block; cursor: pointer; @@ -110,7 +116,7 @@ body.syntax-editor { box-shadow: 2px 2px 4px rgba(0, 0, 0, 0.3); } .refinement.disabled -{ +{ opacity: 0.5; } |
