From 67ca0a1eae3875cb72c4a89fe7d0f454722c3b59 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Fri, 16 Nov 2012 09:33:55 +0000
Subject: Syntax editor: select subset of available languages

Also added a basic readme file with a list of todo's
---
 src/www/syntax-editor/js/editor.js | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/www/syntax-editor/js/editor.js')

diff --git a/src/www/syntax-editor/js/editor.js b/src/www/syntax-editor/js/editor.js
index b7fa2dd87..608770edb 100644
--- a/src/www/syntax-editor/js/editor.js
+++ b/src/www/syntax-editor/js/editor.js
@@ -108,14 +108,16 @@ Editor.prototype.get_refinements=function(cat) {
 
 Editor.prototype.select_refinement=function(fun) {
     with (this) {
+        clear(ui.refinements);
         ast.removeChildren();
         ast.setFun(fun);
+//        redraw_tree();
+
         var args = {
             id: fun,
             format: "json"
         };
         var err = function(data){
-            clear(refinements);
             alert("no refinements");
         };
         server.browse(args, bind(complete_refinement,this), err);
@@ -139,7 +141,7 @@ Editor.prototype.complete_refinement=function(data) {
             }
         }
         
-        // Update vis
+        // Update ui
         redraw_tree();
         update_linearisation();
 
-- 
cgit v1.2.3