1 files changed, 7 insertions, 5 deletions
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();
     }
 }