Syntax editor: jump to next hole in tree

2 files changed, 46 insertions, 6 deletions

diff --git a/src/www/syntax-editor/js/ast.js b/src/www/syntax-editor/js/ast.js
index de9e9d3eb..0bcb75a16 100644
--- a/src/www/syntax-editor/js/ast.js
+++ b/src/www/syntax-editor/js/ast.js
@@ -5,7 +5,8 @@ function Tree(value) {
     var createNode = function(value, children) {
         var node = {
             value: value,
-            children: []
+            children: [],
+            hasChildren: function(){ return this.children.length > 0; }
         };
         if (children != undefined)
             for (c in children)
@@ -106,6 +107,43 @@ function AST(fun, cat) {
         this.tree.find(this.current).children = [];
     }
 
+    // generic HOF for traversing tree
+    this.traverse = function(f) {
+        function visit(id, node) {
+            f(node);
+            for (i in node.children) {
+                var newid = new NodeID(id);
+                newid.add(parseInt(i));
+                visit(newid, node.children[i]);
+            }
+        }
+        visit(new NodeID(), this.tree.root);
+    }
+
+    // Move current ID to next hole
+    this.toNextHole = function() {
+        var id = new NodeID(this.current);
+        
+        // loop until we're at top
+        while (id.get().length > 0) {
+            var node = this.tree.find(id);
+
+            // first check children
+            for (i in node.children) {
+                var child = node.children[i];
+                if (!child.value.fun) {
+                    var newid = new NodeID(id);
+                    newid.add(i);
+                    this.current = newid;
+                    return;
+                }
+            }
+
+            // otherwise go up to parent
+            id.get().pop();
+        }
+    }
+
     // Move current id to child number i
     this.toChild = function(i) {
         this.current.add(i);
diff --git a/src/www/syntax-editor/js/editor.js b/src/www/syntax-editor/js/editor.js
index 740150c18..b7fa2dd87 100644
--- a/src/www/syntax-editor/js/editor.js
+++ b/src/www/syntax-editor/js/editor.js
@@ -137,14 +137,16 @@ Editor.prototype.complete_refinement=function(data) {
             for (ci in fun_args) {
                 ast.add(null, fun_args[ci]);
             }
-
-            // Select next hole & get its refinements
-            ast.toChild(0);
-            update_current_node();
-            get_refinements();
         }
+        
+        // Update vis
         redraw_tree();
         update_linearisation();
+
+        // Select next hole & get its refinements
+        ast.toNextHole();
+        update_current_node();
+        get_refinements();
     }
 }