diff --git a/src/www/syntax-editor/README.md b/src/www/syntax-editor/README.md index 8857bc46a..19e408b1a 100644 --- a/src/www/syntax-editor/README.md +++ b/src/www/syntax-editor/README.md @@ -29,12 +29,15 @@ An improved version of the [old syntax editor][1]. See `editor.html` and `editor_online.js`. +## Bugs + +- Change startcat doesn't work when given an initial startcat + ## TODO - Wrap a subtree - Compatibility with grammars with dependent category types - Clicking on tokens to select tree node -- try to retain subtree when replacing node - Use local caching - Clipboard of trees - Usage of printnames diff --git a/src/www/syntax-editor/ast.js b/src/www/syntax-editor/ast.js index b73448f93..178bc920a 100644 --- a/src/www/syntax-editor/ast.js +++ b/src/www/syntax-editor/ast.js @@ -120,6 +120,29 @@ function AST(fun, cat) { x.children.push(node); } + // Determine if current node is writable (empty/no children) + this.is_writable=function() { + var current = this.getCurrent(); + var blank = current.fun == null || current.children.length == 0; + return blank; + } + + // Determine if a fun would fit in a current hole + this.fits_in_place=function(typeobj) { + var current = this.getCurrent(); + + var inplace = false; + if (typeobj.args.length == current.children.length) { + var matches = 0; + for (var i in typeobj.args) { + if (typeobj.args[i] == current.children[i].cat) + matches++; + } + inplace = matches == current.children.length; + } + return inplace; + } + // Set entire subtree at current node this.setSubtree = function(node) { this._setSubtree(this.current, node); @@ -140,9 +163,9 @@ function AST(fun, cat) { } node.children[lid.shift()] = new ASTNode(subtree); } - } + // Find a node in the tree from its ID this.find = function(id) { var lid = undefined if (Object.prototype.toString.call(id) == "[object Object]") { 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 { diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js index 6290ebd18..355c44082 100644 --- a/src/www/syntax-editor/editor.js +++ b/src/www/syntax-editor/editor.js @@ -119,6 +119,7 @@ Editor.prototype.start_fresh=function () { /* --- Functions for handling tree manipulation ----------------------------- */ +// Show refinements for given cat (usually that of current node) Editor.prototype.get_refinements=function(cat) { var t = this; t.ui.refinements.innerHTML = "..."; @@ -131,10 +132,21 @@ Editor.prototype.get_refinements=function(cat) { var cont = function(data){ clear(t.ui.refinements); for (pi in data.producers) { - var opt = span_class("refinement", text(data.producers[pi])); + var fun = data.producers[pi]; + var opt = span_class("refinement", text(fun)); opt.onclick = bind(function(){ t.select_refinement(this.innerHTML) }, opt); + + // If refinement would be destructive, disable it + var blank = t.ast.is_writable(); + var def = t.grammar_constructors.funs[fun].def; + var typeobj = AST.parse_type_signature(def); + var inplace = t.ast.fits_in_place(typeobj); + if (!blank && !inplace) { + opt.classList.add("disabled"); + } + t.ui.refinements.appendChild(opt); } }; @@ -187,35 +199,55 @@ Editor.prototype.get_refinements=function(cat) { // } // } +// Select refinement now by default replaces "in-place" +// Case 1: current node is blank/no kids +// Case 2: kids have all same types, perform an in-place replacement +// Case 3: kids have diff types/number, prevent replacement (must clear first) Editor.prototype.select_refinement=function(fun) { var t = this; - t.ast.removeChildren(); - t.ast.setFun(fun); + + // Check if current node is blank or childless (case 1) + var blank = t.ast.is_writable(); - // Parse out function arguments + // Check if we can replace in-place (case 2) var def = t.grammar_constructors.funs[fun].def; var typeobj = AST.parse_type_signature(def); + var inplace = !blank && t.ast.fits_in_place(typeobj); - // Add dependent type placeholders - if (typeobj.deps.length > 0) { - for (var i in typeobj.deps) { - t.ast.addDep(typeobj.deps[i].id, typeobj.deps[i].type); + if (!blank && !inplace) { + alert("use clear first if you want to replace the subtree"); + return; + } + + t.ast.setFun(fun); + + if (blank) { + t.ast.removeChildren(); + + // Get new function arguments + var def = t.grammar_constructors.funs[fun].def; + var typeobj = AST.parse_type_signature(def); + + // Add dependent type placeholders + if (typeobj.deps.length > 0) { + alert("the syntax editor current doesn't support dependent types"); + // for (var i in typeobj.deps) { + // t.ast.addDep(typeobj.deps[i].id, typeobj.deps[i].type); + // } + } + // Add function argument placeholders + if (typeobj.args.length > 0) { + for (var i in typeobj.args) { + t.ast.add(null, typeobj.args[i]); + } } } - - // Add function argument placeholders - if (typeobj.args.length > 0) { - for (var i in typeobj.args) { - t.ast.add(null, typeobj.args[i]); - } - } - + // Update ui t.redraw_tree(); t.update_linearisation(); // Select next hole & get its refinements - t.ui.refinements.innerHTML = "..."; t.ast.toNextHole(); t.update_current_node(); } @@ -289,8 +321,8 @@ Editor.prototype.update_linearisation=function(){ }); } -// -Editor.prototype.delete_refinement = function() { +// Clear current node and all its children +Editor.prototype.clear_node = function() { var t = this; t.ast.removeChildren(); t.ast.setFun(null); @@ -342,14 +374,12 @@ Editor.prototype.import_ast = function(abstr) { } // Look up information for a function -// This will absolutely fail on dependant types Editor.prototype.lookup_fun = function(fun) { var t = this; var def = t.grammar_constructors.funs[fun].def; - var ix = def.lastIndexOf(" "); - var cat = def.substr(ix).trim(); + var typeobj = AST.parse_type_signature(def); return { - cat: cat + cat: typeobj.ret } } diff --git a/src/www/syntax-editor/editor_menu.js b/src/www/syntax-editor/editor_menu.js index 31927a26e..57000e551 100644 --- a/src/www/syntax-editor/editor_menu.js +++ b/src/www/syntax-editor/editor_menu.js @@ -28,8 +28,11 @@ function EditorMenu(editor,opts) { multiple: "multiple", class: "hidden" }), + // wrap_button: button("Wrap", function(){ + // t.editor.wrap(); + // }), clear_button: button("Clear", function(){ - t.editor.delete_refinement(); + t.editor.clear_node(); }), random_button: button("Random", function(){ t.editor.generate_random();