summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/www/syntax-editor/README.md5
-rw-r--r--src/www/syntax-editor/ast.js25
-rw-r--r--src/www/syntax-editor/editor.css4
-rw-r--r--src/www/syntax-editor/editor.js74
-rw-r--r--src/www/syntax-editor/editor_menu.js5
5 files changed, 88 insertions, 25 deletions
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;
}
-
- // Add function argument placeholders
- if (typeobj.args.length > 0) {
- for (var i in typeobj.args) {
- t.ast.add(null, typeobj.args[i]);
+
+ 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]);
+ }
}
}
-
+
// 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();