Syntax editor: various small improvements...

- separate tree edit buttons from option buttons
- fix bug when wrapping on freshly imported ast
- add interface for import & export of ast
- cleaner internal implementation of Editor.add_refinement
- small style updates

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
 {