Syntax editor: AST string always shown, remove export button

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;
   }
 

src/www/syntax-editor/editor.js

@@ -33,6 +33,8 @@ function Editor(gm,opts) {
 
         tree: div_id("tree"),
 
+        tree_str: div_id("tree_str"),
+
         actionbar: div_id("actions"),
         clear_button: button("Clear", function(){
             t.clear_node();
@@ -51,10 +53,11 @@ function Editor(gm,opts) {
     this.ui.clear_button.title = "Clear current node and all its children";
     this.ui.wrap_button.title = "Wrap the current node with a new function";
     this.ui.unwrap_button.title = "Replace parent of current node with current node (if possible)";
-    
+
     appendChildren(this.container, [
         t.ui.menubar,
         t.ui.tree,
+        t.ui.tree_str,
         t.ui.actionbar,
         t.ui.lin
     ]);
@@ -266,7 +269,7 @@ Editor.prototype.get_refinements=function(cat) {
 // Case 3: kids have diff types/number, prevent replacement (must clear first)
 Editor.prototype.select_refinement=function(fun) {
     var t = this;
-    
+
     // Check if current node is blank or childless (case 1)
     var blank = t.ast.is_writable();
 
@@ -427,7 +430,7 @@ Editor.prototype.unwrap = function() {
         alert("It is not possible to unwrap the top node");
         return;
     }
-    
+
     var child = t.ast.getCurrentNode();
     var parent = t.ast.getParent();
 
@@ -519,6 +522,7 @@ Editor.prototype.redraw_tree=function() {
     }
     with(this) {
         clear(ui.tree);
+        ui.tree_str.innerText = ast.toString();
         visit(ui.tree, new NodeID(), ast.root);
     }
 }
@@ -582,4 +586,3 @@ Editor.prototype.import_ast = function(abstr) {
     };
     t.server.pgf_call("abstrjson", args, cont, err);
 }
-

src/www/syntax-editor/editor_menu.js

@@ -11,7 +11,6 @@ function EditorMenu(editor,opts) {
         show_to_menu: true,
         show_random_button: true,
         show_import: true,
-        show_export: true,
     }
 
     // Apply supplied options
@@ -47,9 +46,7 @@ function EditorMenu(editor,opts) {
                 toggleHidden(t.ui.import.panel);
             })
         },
-        export_button: button("Export", function(){
-            alert(t.editor.ast.toString());
-        }),
+
         debug_toggle: button("⚙", function(){
             toggleHidden(element("debug"));
         })
@@ -57,7 +54,6 @@ function EditorMenu(editor,opts) {
     this.ui.to_toggle.title = "Select languages to linearise to (use Ctrl/Shift to select multiple)";
     this.ui.random_button.title = "Insert a randomly generated tree at the current node";
     this.ui.import.toggle.title = "Import an abstract syntax tree from a string (replaces current tree)";
-    this.ui.export_button.title = "Get the string representation of the abstract syntax tree";
     this.ui.debug_toggle.title = "Toggle the debug console";
 
     if (t.options.show_grammar_menu) {
@@ -95,11 +91,7 @@ function EditorMenu(editor,opts) {
             t.ui.import.button
         ]);
     }
-    if (t.options.show_export) {
-        appendChildren(t.container, [
-            t.ui.export_button,
-        ]);
-    }
+
     appendChildren(t.container, [t.ui.debug_toggle]);
 
     /* --- Client state initialisation -------------------------------------- */
@@ -187,7 +179,7 @@ EditorMenu.prototype.update_language_menu=function(menu,grammar) {
     // Replace the options in the menu with the languages in the grammar
     var langs=grammar.languages;
     menu.innerHTML="";
-	
+
     for(var i=0; i<langs.length; i++) {
 	var ln=langs[i].name;
 	if(!hasPrefix(ln,"Disamb")) {
@@ -200,4 +192,3 @@ EditorMenu.prototype.update_language_menu=function(menu,grammar) {
 	}
     }
 }
-