diff options
Diffstat (limited to 'src/www/syntax-editor/editor.css')
| -rw-r--r-- | src/www/syntax-editor/editor.css | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/www/syntax-editor/editor.css b/src/www/syntax-editor/editor.css index f36898d5c..6d4511eb0 100644 --- a/src/www/syntax-editor/editor.css +++ b/src/www/syntax-editor/editor.css @@ -14,6 +14,27 @@ body.syntax-editor { min-width: 5em; } +#import +{ + position: absolute; + display: inline-block; + padding: 0.3em; + background: #EEE; + border: 1px solid #999; + font-size: 0.95em; + box-shadow: 2px 2px 4px rgba(0, 0, 0, 0.3); + } +#import.hidden +{ + display: none; + } +#import input[type=text] +{ + width: 20em; + font-family: monospace; + padding: 0.2em; + } + #tree { white-space:pre; @@ -41,6 +62,13 @@ body.syntax-editor { font-weight: bold; } +#refinements +{ + /* display: inline-block; */ + /* margin-left: 0.5em; */ + margin-top: 0.3em; + } + #linearisations { /* background: rgba(170, 170, 170, 0.5); */ @@ -65,13 +93,14 @@ body.syntax-editor { .refinement { - margin: 0 0.1em; + margin: 0.1em; display: inline-block; cursor: pointer; border: 1px solid; padding: 0.2em; font: 0.9em sans-serif; background: white; + box-shadow: 2px 2px 4px rgba(0, 0, 0, 0.3); } .refinement.disabled { |