diff --git a/src/www/syntax-editor/ast.js b/src/www/syntax-editor/ast.js index 026452697..ed8235a79 100644 --- a/src/www/syntax-editor/ast.js +++ b/src/www/syntax-editor/ast.js @@ -94,6 +94,15 @@ function AST(fun, cat) { this.currentNode = this.find(this.currentID); } + this.hasParent = function() { + return this.currentID.get().length > 1; + // return !this.atRoot(); + } + this.atRoot = function() { + return this.currentNode == this.root; + // return !this.hasParent(); + } + this.getFun = function() { return this.currentNode.fun; } @@ -107,10 +116,6 @@ function AST(fun, cat) { this.currentNode.cat = c; } - this.hasParent = function() { - return this.currentID.get().length > 1; - } - // Add a single type dependency at current node this.addDep = function(k, type) { // Add unassigned type variable to current @@ -140,7 +145,7 @@ function AST(fun, cat) { // Doesn't check whether child_id is within in range this.wrap = function(typeobj, child_id) { var subtree = new ASTNode(this.currentNode); - this.currentNode.fun = typeobj.name.join(" "); + this.currentNode.fun = typeobj.name; this.currentNode.cat = typeobj.ret; this.currentNode.children = []; for (var i in typeobj.args) { @@ -185,15 +190,14 @@ function AST(fun, cat) { if (lid.length==1) { // Insert at root - this.root = new ASTNode(subtree); - this.currentNode = this.root; + this.currentNode = this.root = new ASTNode(subtree); } else { lid.shift(); // throw away root while (lid.length>1 && node.hasChildren()) { node = node.children[lid.shift()]; } - node.children[lid.shift()] = new ASTNode(subtree); + this.currentNode = node.children[lid.shift()] = new ASTNode(subtree); } } @@ -301,7 +305,7 @@ AST.parse_type_signature = function(str) { var obj = { signature: str, type: undefined, - name: [], + name: undefined, deps: [], args: [], ret: undefined @@ -313,7 +317,7 @@ AST.parse_type_signature = function(str) { obj.type = bits[0]; // name (possibly with constructors) - obj.name = bits.slice(1); + obj.name = bits.slice(1).join(" "); // function args (possibly with type dependency) var regex_dep = new RegExp(/\(\s*(.+?)\s*:\s*(.+?)\s*\)/); diff --git a/src/www/syntax-editor/editor.css b/src/www/syntax-editor/editor.css index 6d4511eb0..6a23c5bd4 100644 --- a/src/www/syntax-editor/editor.css +++ b/src/www/syntax-editor/editor.css @@ -46,7 +46,14 @@ body.syntax-editor { #tree .node { - margin: 0.4em 0 0.4em 1.5em; + margin: 0.5em 0 0.5em 0.75em; + border-left: 1px dashed #BBB; + padding-left: 1.25em; + } +#tree .node.first +{ + margin-left: 0; + border-left: none; } #tree .node a @@ -72,7 +79,7 @@ body.syntax-editor { #linearisations { /* background: rgba(170, 170, 170, 0.5); */ - padding:0.5em; + /* padding:0.5em; */ margin:0.5em 0; } #linearisations div diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js index 65fe6c00f..1dd858f21 100644 --- a/src/www/syntax-editor/editor.js +++ b/src/www/syntax-editor/editor.js @@ -64,6 +64,7 @@ function Editor(gm,opts) { this.gm = gm; this.server = gm.server; this.ast = null; + this.clear_on_change_startcat = true; // temp. false when wrapping /* --- Register Grammar Manager hooks ----------------------------------- */ this.hook_change_grammar = function(grammar){ @@ -80,7 +81,8 @@ function Editor(gm,opts) { this.hook_change_startcat = function(startcat){ debug("Editor: change startcat"); t.startcat = startcat; - t.start_fresh(); + if (t.clear_on_change_startcat) + t.start_fresh(); }; this.hook_change_languages = function(languages){ debug("Editor: change languages"); @@ -167,7 +169,7 @@ Editor.prototype.add_refinement=function(fun,opts) { var t = this; options = { label: fun, - disable_destructive: true + disable_destructive: false }; if (opts) for (var o in opts) options[o] = opts[o]; var typeobj = t.lookup_fun(fun); @@ -296,12 +298,12 @@ Editor.prototype.wrap_candidates = function() { // we need to end with this var cat = t.ast.getCat(); - // if no parent, then cat can be anything as long - // as the current tree fits somewhere var refinements = []; for (var i in t.grammar_constructors.funs) { var obj = t.grammar_constructors.funs[i]; if (elem(cat, obj.args)) { + // if no parent, then cat can be anything + // as long as the current tree fits somewhere if (!t.ast.hasParent() || obj.ret==cat) { refinements.push(obj); } @@ -313,27 +315,46 @@ Editor.prototype.wrap_candidates = function() { return; } + // Display wrap refinements + function addClickHandler(fun, child_id) { + return function() { + t.wrap.apply(t,[fun, child_id]); + } + } t.ui.refinements.innerHTML = "Wrap with: "; for (var i in refinements) { var typeobj = refinements[i]; + var fun = typeobj.name; - // Show a refinement for each potential child position - function addClickHandler(fun, child_id) { - return function() { - t.wrap.apply(t,[fun, child_id]); - } - } + // Find valid child ids + var child_ids = []; for (var a in typeobj.args) { - var arg = typeobj.args[a]; - if (arg == cat) { - var label = typeobj.name + " ?" + (parseInt(a)+1); - var ref = t.add_refinement(typeobj.name, { - label: label, - disable_destructive: false, - }); - ref.onclick = addClickHandler(typeobj.name, a); + if (typeobj.args[a] == cat) { + child_ids.push(a); } } + + // if (child_ids.length < 2) { + // var ref = t.add_refinement(fun); + // ref.onclick = addClickHandler(typeobj.name, a); + // } else { + // Show a refinement for each potential child position + for (var c in child_ids) { + var id = child_ids[c]; + var label = fun; + for (var a in typeobj.args) { + if (a == id) + if (t.ast.currentNode.hasChildren()) + label += " ("+t.ast.currentNode.fun+" …)"; + else + label += " "+t.ast.currentNode.fun; + else + label += " ?"; + } + var ref = t.add_refinement(typeobj.name, {label: label}); + ref.onclick = addClickHandler(typeobj.name, id); + } + // } } } @@ -342,6 +363,14 @@ Editor.prototype.wrap = function(fun, child_id) { var t = this; var typeobj = t.grammar_constructors.funs[fun]; + // if we are at root node, potentially change startcat + if (t.ast.atRoot() && t.get_startcat() != typeobj.ret) { + var old_val = t.clear_on_change_startcat; + t.clear_on_change_startcat = false; + t.gm.change_startcat(typeobj.ret); + t.clear_on_change_startcat = old_val; + } + // do actual replacement t.ast.wrap(typeobj, child_id); @@ -380,6 +409,8 @@ Editor.prototype.redraw_tree=function() { var elem = node; // function from support.js function visit(container, id, node) { var container2 = empty_class("div", "node"); + if (id.get().length == 1) + container2.classList.add("first"); var label = ((node.fun) ? node.fun : "?") + " : " + ((node.cat) ? node.cat : "?"); diff --git a/src/www/syntax-editor/editor_menu.js b/src/www/syntax-editor/editor_menu.js index b5ceedd77..2b9ee8d59 100644 --- a/src/www/syntax-editor/editor_menu.js +++ b/src/www/syntax-editor/editor_menu.js @@ -109,6 +109,7 @@ function EditorMenu(editor,opts) { /* --- Register Grammar Manager hooks ----------------------------------- */ this.gm.register_action("onload", bind(this.hook_onload, this)); this.gm.register_action("change_grammar", bind(this.hook_change_grammar, this)); + this.gm.register_action("change_startcat", bind(this.hook_change_startcat, this)); } @@ -143,16 +144,11 @@ EditorMenu.prototype.hook_onload=function(dir,grammar_names,dir_count) { } // Copied from minibar.js -EditorMenu.prototype.hook_change_grammar=function() { +EditorMenu.prototype.hook_change_grammar=function(grammar) { debug("EditorMenu: change grammar"); var t=this; - var grammar_url = t.ui.grammar_menu.value; - t.server.switch_to_other_grammar(grammar_url, function() { - t.server.grammar_info(function(grammar){ - t.update_startcat_menu(grammar); - t.update_language_menu(t.ui.to_menu, grammar); - }); - }); + t.update_startcat_menu(grammar); + t.update_language_menu(t.ui.to_menu, grammar); } /* --- Start category menu -------------------------------------------------- */ @@ -171,6 +167,14 @@ EditorMenu.prototype.update_startcat_menu=function(grammar) { menu.value = grammar.startcat; } +// If startcat changed externally, update menu +EditorMenu.prototype.hook_change_startcat=function(startcat) { + debug("EditorMenu: change startcat"); + var t=this; + var menu=this.ui.startcat_menu; + menu.value = startcat; +} + /* --- Langugage (to) menu -------------------------------------------------- */ // Called from hook_change_grammar