From c505747492e8ee96ef143f7f464bbf8671c21b58 Mon Sep 17 00:00:00 2001 From: "john.j.camilleri" Date: Thu, 13 Jun 2013 07:26:10 +0000 Subject: Syntax editor: AST string always shown, remove export button --- src/www/syntax-editor/editor.js | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/www/syntax-editor/editor.js') diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js index be6b84820..16ccc1533 100644 --- a/src/www/syntax-editor/editor.js +++ b/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); } - -- cgit v1.2.3