diff options
| author | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-30 10:56:42 +0000 |
|---|---|---|
| committer | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-30 10:56:42 +0000 |
| commit | 58c3e3db85d55cc9b746732583df83c19a9b68e0 (patch) | |
| tree | 1acc94a1d19dce79c92c2c968960037908e28e4d /src/www/syntax-editor/editor.css | |
| parent | 3c900ee6a3a31ba8a438d876ad8cfd352e97608a (diff) | |
Syntax editor: in-place replacement of functions
When at a non-leaf node, refinements with identical type signatures
are highlighting and can re placed without destroying the children.
If not, the refinement is greyed and the user is asked to clear
the current subtree first if they wish to replace it.
This aspect of the UI should be polished, but at least it is obvious.
Also, some substantial optimizations can still be made to cache
the processed type signatures (which determine what can be replaced
in-place)
Diffstat (limited to 'src/www/syntax-editor/editor.css')
| -rw-r--r-- | src/www/syntax-editor/editor.css | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/www/syntax-editor/editor.css b/src/www/syntax-editor/editor.css index 2257db6e8..f36898d5c 100644 --- a/src/www/syntax-editor/editor.css +++ b/src/www/syntax-editor/editor.css @@ -73,6 +73,10 @@ body.syntax-editor { font: 0.9em sans-serif; background: white; } +.refinement.disabled +{ + opacity: 0.5; + } #debug { |