From 48dbabcbbe0c3465d6c6cd96a7a0a0a0662d8774 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Thu, 15 Nov 2012 15:38:17 +0000
Subject: [PATCH] Syntax editor: jump to next hole in tree

---
 src/www/syntax-editor/js/ast.js    | 40 +++++++++++++++++++++++++++++-
 src/www/syntax-editor/js/editor.js | 12 +++++----
 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();
     }
 }