From 7a69d9d5e5800a1d4e523b487bba3969e6f2a998 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Tue, 13 Nov 2012 15:14:49 +0000
Subject: [PATCH] Add first demo of new syntax editor

As part of the GF cloud stuff, it can be accessed from
http://cloud.grammaticalframework.org/syntax-editor/editor.html
---
 gf.cabal                                |   3 +
 src/www/index.html                      |   3 +-
 src/www/syntax-editor/editor.html       |  43 ++++
 src/www/syntax-editor/js/ast.js         | 131 ++++++++++
 src/www/syntax-editor/js/editor.js      | 216 ++++++++++++++++
 src/www/syntax-editor/js/editor_menu.js | 153 +++++++++++
 src/www/syntax-editor/js/pgf_online.js  |  80 ++++++
 src/www/syntax-editor/js/support.js     | 329 ++++++++++++++++++++++++
 src/www/syntax-editor/ui/style.css      |  64 +++++
 9 files changed, 1021 insertions(+), 1 deletion(-)
 create mode 100644 src/www/syntax-editor/editor.html
 create mode 100644 src/www/syntax-editor/js/ast.js
 create mode 100644 src/www/syntax-editor/js/editor.js
 create mode 100644 src/www/syntax-editor/js/editor_menu.js
 create mode 100644 src/www/syntax-editor/js/pgf_online.js
 create mode 100644 src/www/syntax-editor/js/support.js
 create mode 100644 src/www/syntax-editor/ui/style.css
diff --git a/gf.cabal b/gf.cabal
index 52e785430..c979cdb88 100644
--- a/gf.cabal
+++ b/gf.cabal
@@ -24,6 +24,9 @@ data-files: www/*.html
 	    www/minibar/*.css
 	    www/minibar/*.js
 	    www/minibar/*.png
+	    www/syntax-editor/*.html
+	    www/syntax-editor/ui/*.css
+	    www/syntax-editor/js/*.js
 	    www/TransQuiz/*.html
 	    www/TransQuiz/*.css
 	    www/TransQuiz/*.js
diff --git a/src/www/index.html b/src/www/index.html
index df50c4dbe..c1e62bf45 100644
--- a/src/www/index.html
+++ b/src/www/index.html
@@ -13,6 +13,7 @@
 
 <ul>
   <li><a href="minibar/minibar.html">Minibar</a>
+  <li><a href="syntax-editor/editor.html">Syntax Editor (beta)</a>
   <li><a href="TransQuiz/translation_quiz.html">Translation Quiz</a>
   <li><a href="gfse/">GF online editor for simple multilingual grammars</a>
   <li><a href="translator/">Simple Translation Tool</a>
@@ -33,4 +34,4 @@
 <hr>
 
 <a href="http://www.grammaticalframework.org/">www.grammaticalframework.org</a>
-<div class=modtime><small><a href="/version">GF version</a></small></div>
\ No newline at end of file
+<div class=modtime><small><a href="/version">GF version</a></small></div>
diff --git a/src/www/syntax-editor/editor.html b/src/www/syntax-editor/editor.html
new file mode 100644
index 000000000..d641998ab
--- /dev/null
+++ b/src/www/syntax-editor/editor.html
@@ -0,0 +1,43 @@
+<!doctype html>
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <link rel="author" href="http://www.grammaticalframework.org/~john/" title="John J. Camilleri">
+  <title>Syntax Editor</title>
+  <link rel="stylesheet" type="text/css" href="http://cloud.grammaticalframework.org/minibar/minibar.css" />
+  <link rel="stylesheet" type="text/css" href="ui/style.css" />
+</head>
+<body>
+  <h2>Syntax Editor</h2>
+  <div id="editor"></div>
+  <noscript>This page doesn't works unless JavaScript is enabled.</noscript>
+
+  <hr />
+  <small class="modtime">
+  John J. Camilleri, November 2012
+  </small>
+
+  <script type="text/javascript" src="js/support.js"></script>
+  <script type="text/javascript" src="js/pgf_online.js"></script>
+  <script type="text/javascript" src="js/ast.js"></script>
+  <script type="text/javascript" src="js/editor_menu.js"></script>
+  <script type="text/javascript" src="js/editor.js"></script>
+  <script type="text/javascript">
+    // Code taken from minibar_online.js
+    var server_options = {
+        //grammars_url: "http://www.grammaticalframework.org/grammars/",
+        //grammars_url: "http://localhost:41296/grammars/",
+    }
+    var editor_options = {
+	target: "editor"
+    }
+    if(/^\?\/tmp\//.test(location.search)) {
+        var args=decodeURIComponent(location.search.substr(1)).split(" ")
+        if(args[0]) server_options.grammars_url=args[0];
+    }
+    var server = pgf_online(server_options);
+    var editor = new Editor(server, editor_options);
+  </script>
+  
+</body>
+</html>
diff --git a/src/www/syntax-editor/js/ast.js b/src/www/syntax-editor/js/ast.js
new file mode 100644
index 000000000..de9e9d3eb
--- /dev/null
+++ b/src/www/syntax-editor/js/ast.js
@@ -0,0 +1,131 @@
+/* --- Tree representation -------------------------------------------------- */
+function Tree(value) {
+
+    // Create node as JS object
+    var createNode = function(value, children) {
+        var node = {
+            value: value,
+            children: []
+        };
+        if (children != undefined)
+            for (c in children)
+                node.children.push( createNode(children[c],[]) );
+        return node;
+    }
+
+    this.root = createNode(value, []);
+
+    // add value as child of id
+    this.add = function(id, value, children) {
+        var x = this.find(id);
+        x.children.push( createNode(value, children) );
+    }
+
+    // id should be a list of child indices [0,1,0]
+    // or a string separated by commas "0,1,0"
+    this.find = function(_id) {
+        var id = undefined
+        switch (typeof _id) {
+        case "number": id = [_id]; break;
+        case "string": id = _id.split(","); break;
+        case "object": id = _id.get().slice(); break; // clone NodeID array
+        }
+        var node = this.root;
+        if (id[0] == 0) id.shift();
+        while (id.length>0 && node.children.length>0) {
+            node = node.children[id.shift()];
+        }
+        if (id.length>0)
+            return undefined;
+        return node;
+    }
+}
+
+/* --- ID for a node in a tree ---------------------------------------------- */
+function NodeID(x) {
+    this.id = new Array();
+    this.id.push(0);
+
+    // Initialize from input
+    if (x) {
+        switch (typeof x) {
+        case "number": this.id = [x]; break;
+        case "string": this.id = map(function(s){return parseInt(s)}, x.split(",")); break;
+        case "object": this.id = x.get().slice(); break; // another NodeID
+        }
+    }
+
+    // get id
+    this.get = function() {
+        return this.id;
+    }
+    
+    // Add child node to id
+    this.add = function(x) {
+        this.id.push(parseInt(x));
+        return this.id;
+    }
+
+    // compare with other id
+    this.equals = function(other) {
+        return JSON.stringify(this.id)==JSON.stringify(other.id);
+    }
+
+}
+
+/* --- Abstract Syntax Tree (with state)------------------------------------- */
+function AST(fun, cat) {
+
+    function Node(fun, cat) {
+        this.fun = fun;
+        this.cat = cat;
+    }
+
+    this.tree = new Tree(new Node(fun, cat));
+    this.current = new NodeID(); // current id in tree
+
+    this.getFun = function() {
+        return this.tree.find(this.current).value.fun;
+    }
+    this.setFun = function(f) {
+        this.tree.find(this.current).value.fun = f;
+    }
+    this.getCat = function() {
+        return this.tree.find(this.current).value.cat;
+    }
+    this.setCat = function(c) {
+        this.tree.find(this.current).value.cat = c;
+    }
+
+    this.add = function(fun, cat) {
+        this.tree.add(this.current, new Node(fun,cat));
+    }
+    
+    // Clear children of current node
+    this.removeChildren = function() {
+        this.tree.find(this.current).children = [];
+    }
+
+    // Move current id to child number i
+    this.toChild = function(i) {
+        this.current.add(i);
+    }
+
+    // Return tree as string
+    this.toString = function() {
+        var s = "";
+        function visit(node) {
+            s += node.value.fun ? node.value.fun : "?" ;
+            if (node.children.length == 0)
+                return;
+            for (i in node.children) {
+            s += "(";
+                visit(node.children[i]);
+            s += ")";
+            }
+        }
+        visit(this.tree.root);
+        return s;
+    }
+}
+
diff --git a/src/www/syntax-editor/js/editor.js b/src/www/syntax-editor/js/editor.js
new file mode 100644
index 000000000..21f801db0
--- /dev/null
+++ b/src/www/syntax-editor/js/editor.js
@@ -0,0 +1,216 @@
+
+/* --- Some enhancements  --------------------------------------------------- */
+
+// http://www.xenoveritas.org/blog/xeno/the-correct-way-to-clone-javascript-arrays
+// Array.prototype.clone = function(){
+//     return this.slice(0);
+// }
+
+/* --- Main Editor object --------------------------------------------------- */
+function Editor(server,opts) {
+    var t = this;
+    /* --- Configuration ---------------------------------------------------- */
+
+    // default values for options:
+    this.options={
+	target: "editor"
+    }
+
+    // Apply supplied options
+    if(opts) for(var o in opts) this.options[o]=opts[o];
+
+    /* --- Creating UI components ------------------------------------------- */
+    var main = document.getElementById(this.options.target);
+    this.ui = {
+        menubar: div_class("menu"),
+        tree: div_id("tree"),
+        refinements: div_id("refinements"),
+        lin: div_id("linearisations")
+    };
+    with(this.ui) {
+	appendChildren(main, [menubar, tree, refinements, lin]);
+    }
+
+    /* --- Client state initialisation -------------------------------------- */
+    this.server = server;
+    this.ast = null;
+    this.grammar = null;
+    this.languages = [];
+    this.local = {}; // local settings which may override grammar
+
+    /* --- Main program, this gets things going ----------------------------- */
+    this.menu = new EditorMenu(this);
+
+}
+
+/* --- API for getting and setting state ------------------------------------ */
+
+Editor.prototype.get_ast=function() {
+    return this.ast.toString();
+}
+
+Editor.prototype.get_startcat=function() {
+    return this.local.startcat || this.grammar.startcat;
+}
+
+/* --- These get called from EditorMenu, or some custom code                  */
+
+Editor.prototype.change_grammar=function(grammar_info) {
+    with(this) {
+        grammar = grammar_info;
+        local.startcat = null;
+        start_fresh();
+    }
+}
+
+Editor.prototype.change_startcat=function(startcat) {
+    with(this) {
+        local.startcat = startcat;
+        start_fresh();
+    }
+}
+
+// Called after changing grammar or startcat
+Editor.prototype.start_fresh=function () {
+    with(this) {
+        ast = new AST(null, get_startcat());
+        redraw_tree();
+        update_current_node();
+        get_refinements();
+        clear(ui.lin);
+    }
+}
+
+/* --- Functions for handling tree manipulation ----------------------------- */
+
+Editor.prototype.get_refinements=function(cat) {
+    with (this) {
+        if (cat == undefined)
+            cat = ast.getCat();
+        var args = {
+            id: cat,
+            format: "json"
+        };
+        var cont = function(data){
+            clear(refinements);
+            for (pi in data.producers) {
+                var opt = span_class("refinement", text(data.producers[pi]));
+                opt.onclick = function(){ select_refinement(this.innerText) };
+                refinements.appendChild(opt);
+            }
+        };
+        var err = function(data){
+            clear(refinements);
+            alert("no refinements");
+        };
+        server.browse(args,cont,err);
+    }
+}
+
+Editor.prototype.select_refinement=function(fun) {
+    with (this) {
+        ast.removeChildren();
+        ast.setFun(fun);
+        var args = {
+            id: fun,
+            format: "json"
+        };
+        var err = function(data){
+            clear(refinements);
+            alert("no refinements");
+        };
+        server.browse(args, bind(complete_refinement,this), err);
+    }
+}
+
+Editor.prototype.complete_refinement=function(data) {
+    if (!data) return;
+
+    with (this) {
+        // Parse out function arguments
+        var def = data.def;
+        def = def.substr(def.lastIndexOf(":")+1);
+        var fun_args = map(function(s){return s.trim()}, def.split("->"))
+        fun_args = fun_args.slice(0,-1);
+
+        if (fun_args.length > 0) {
+            // Add placeholders
+            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();
+        }
+        redraw_tree();
+        update_linearisation();
+    }
+}
+
+Editor.prototype.update_current_node=function(newID) {
+    with(this) {
+        if (newID)
+            ast.current = new NodeID(newID);
+        redraw_tree();
+        get_refinements();
+    }
+}
+
+Editor.prototype.redraw_tree=function() {
+    var t = this;
+    var elem = node; // function from support.js
+    function visit(container, id, node) {
+        var container2 = empty_class("div", "node");
+        var label = ((node.value.fun) ? node.value.fun : "?") + " : " + node.value.cat;
+        var current = id.equals(t.ast.current);
+        var element = elem("a", {class:(current?"current":"")}, [text(label)]);
+        element.onclick = function() {
+            t.update_current_node(id);
+        }
+        container2.appendChild( element );
+
+        for (i in node.children) {
+            var newid = new NodeID(id);
+            newid.add(parseInt(i));
+            visit(container2, newid, node.children[i]);
+        }
+
+        container.appendChild(container2);
+    }
+    with(this) {
+        clear(ui.tree);
+        visit(ui.tree, new NodeID(), ast.tree.root);
+    }
+}
+
+Editor.prototype.update_linearisation=function(){
+
+    function langpart(conc,abs) { // langpart("FoodsEng","Foods") == "Eng"
+        return hasPrefix(conc,abs) ? conc.substr(abs.length) : conc;
+    }
+
+    var t = this;
+    with (this) {
+        var args = {
+            tree: ast.toString()
+        };
+        server.linearize(args, function(data){
+            clear(t.ui.lin);
+            for (i in data) {
+                var lang = data[i].to;
+                var langname = langpart(lang, t.grammar.name);
+                if (t.languages.length < 1 || elem(lang, t.languages)) {
+                    var div_lang = empty("div");
+                    div_lang.appendChild(span_class("lang", text(langname)));
+                    div_lang.appendChild(
+                        span_class("lin", [text(data[i].text)])
+                    );
+                    t.ui.lin.appendChild(div_lang);
+                }
+            }
+        });
+    }
+}
+
diff --git a/src/www/syntax-editor/js/editor_menu.js b/src/www/syntax-editor/js/editor_menu.js
new file mode 100644
index 000000000..874859ae7
--- /dev/null
+++ b/src/www/syntax-editor/js/editor_menu.js
@@ -0,0 +1,153 @@
+/* --- Editor Menu object --------------------------------------------------- */
+function EditorMenu(editor,opts) {
+    var t = this;
+    /* --- Configuration ---------------------------------------------------- */
+
+    // default values for options:
+    this.options={
+	target: "editor"
+    }
+
+    // Apply supplied options
+    if(opts) for(var o in opts) this.options[o]=opts[o];
+
+    /* --- Creating UI components ------------------------------------------- */
+    this.container = editor.ui.menubar;
+    this.ui = {
+        startcat_menu: empty("select"),
+        to_menu: empty_id("select","to_menu")
+    };
+    with(this.ui) {
+	appendChildren(this.container, [text(" Startcat: "),startcat_menu]);
+        appendChildren(this.container, [text(" To: "), to_menu]);
+        startcat_menu.onchange=bind(this.change_startcat,this);
+        to_menu.onchange=bind(this.change_language,this);
+    }
+
+    /* --- Client state initialisation -------------------------------------- */
+    this.editor = editor;
+    this.server = editor.server;
+
+    /* --- Main program, this gets things going ----------------------------- */
+    with(this) {
+	server.get_grammarlists(bind(show_grammarlist,this));
+    }
+}
+
+// Copied from minibar.js
+EditorMenu.prototype.show_grammarlist=function(dir,grammar_names,dir_count) {
+    var t=this;
+    var first_time= !t.grammar_menu
+    if(first_time) {
+	t.grammar_menu=empty_id("select","grammar_menu");
+	t.grammars=[];
+	t.grammar_dirs=[];
+    }
+    with(t) {
+	grammar_dirs.push(dir);
+	grammars=grammars.concat(grammar_names.map(function(g){return dir+g}))
+	function glabel(g) {
+	    return hasPrefix(dir,"/tmp/gfse.") ? "gfse: "+g : g
+	}
+	function opt(g) { return option(glabel(g),dir+g); }
+	appendChildren(grammar_menu,map(opt,grammar_names));
+	function pick() {
+	    var grammar_url=grammar_menu.value
+	    if(window.localStorage)
+		localStorage["gf.minibar.last_grammar"]=grammar_url;
+	    t.select_grammar(grammar_url);
+	}
+	function pick_first_grammar() {
+	    if(t.timeout) clearTimeout(t.timeout),t.timeout=null;
+	    if(t.grammar_menu.length>1 && !t.grammar_menu.parentElement) {
+    		t.grammar_menu.onchange=pick;
+//		insertFirst(t.menubar,button("i",bind(t.show_grammarinfo,t)))
+		insertFirst(t.container,t.grammar_menu);
+		insertFirst(t.container,text("Grammar: "));
+	    }
+	    var grammar0=t.options.initial_grammar
+	    if(!grammar0 && window.localStorage) {
+		var last_grammar=localStorage["gf.minibar.last_grammar"];
+		if(last_grammar && elem(last_grammar,t.grammars))
+		    grammar0=last_grammar;
+	    }
+	    if(!grammar0) grammar0=t.grammars[0];
+	    t.grammar_menu.value=grammar0;
+	    t.select_grammar(grammar0);
+	}
+	// Wait at most 1.5s before showing the grammar menu.
+	if(first_time) t.timeout=setTimeout(pick_first_grammar,1500);
+	if(t.grammar_dirs.length>=dir_count) pick_first_grammar();
+    }
+}
+
+// Copied from minibar.js
+EditorMenu.prototype.select_grammar=function(grammar_url) {
+    var t=this;
+    //debug("select_grammar ");
+    t.server.switch_to_other_grammar(grammar_url, function() {
+	t.server.grammar_info(function(grammar){
+            t.update_language_menu(t.ui.to_menu, grammar);
+            t.update_startcat_menu(grammar);
+
+            // Call in main Editor object
+            t.editor.change_grammar(grammar);
+        });
+    });
+}
+
+// Copied from minibar_input.js
+EditorMenu.prototype.update_startcat_menu=function(grammar) {
+    var menu=this.ui.startcat_menu;
+    menu.innerHTML="";
+    var cats=grammar.categories;
+    for(var cat in cats) menu.appendChild(option(cats[cat],cats[cat]))
+//    var startcat=this.local.get("startcat") || grammar.startcat;
+    var startcat= grammar.startcat;
+    if(startcat) menu.value=startcat;
+    else {
+	insertFirst(menu,option("Default",""));
+	menu.value="";
+    }
+}
+
+// 
+EditorMenu.prototype.change_startcat=function () {
+    var new_startcat = this.ui.startcat_menu.value;
+    this.editor.change_startcat(new_startcat);
+}
+
+// 
+EditorMenu.prototype.change_language=function () {
+    if (this.ui.to_menu.value == "All")
+        this.editor.languages = new Array();
+    else
+        this.editor.languages = new Array(this.ui.to_menu.value);
+    this.editor.update_linearisation();
+}
+
+// Copied from minibar_support.js
+EditorMenu.prototype.update_language_menu=function(menu,grammar) {
+
+    function langpart(conc,abs) { // langpart("FoodsEng","Foods") == "Eng"
+        return hasPrefix(conc,abs) ? conc.substr(abs.length) : conc;
+    }
+
+    // Replace the options in the menu with the languages in the grammar
+    var lang=grammar.languages;
+    menu.innerHTML="";
+	
+    for(var i=0; i<lang.length; i++) {
+	var ln=lang[i].name;
+	if(!hasPrefix(ln,"Disamb")) {
+	    var lp=langpart(ln,grammar.name);
+	    menu.appendChild(option(lp,ln));
+	}
+    }
+
+    insertFirst(menu,option("All","All"));
+    menu.value="All";
+}
+
+
+
diff --git a/src/www/syntax-editor/js/pgf_online.js b/src/www/syntax-editor/js/pgf_online.js
new file mode 100644
index 000000000..6fe23b13e
--- /dev/null
+++ b/src/www/syntax-editor/js/pgf_online.js
@@ -0,0 +1,80 @@
+
+/* --- Grammar access object ------------------------------------------------ */
+
+function pgf_online(options) {
+    var server = {
+	// State variables (private):
+	grammars_url: "/grammars/",
+	other_grammars_urls: [],
+	grammar_list: null,
+	current_grammar_url: null,
+
+	// Methods:
+	switch_grammar: function(grammar_url,cont) {
+ 	    this.current_grammar_url=this.grammars_url+grammar_url;
+	    if(cont) cont();
+	},
+	add_grammars_url: function(grammars_url,cont) {
+	    this.other_grammars_urls.push(grammars_url);
+	    if(cont) cont();
+	},
+	switch_to_other_grammar: function(grammar_url,cont) {
+ 	    this.current_grammar_url=grammar_url;
+	    if(cont) cont();
+	},
+	get_grammarlist: function(cont,err) {
+	    if(this.grammar_list) cont(this.grammar_list)
+	    else http_get_json(this.grammars_url+"grammars.cgi",cont,err);
+	},
+	get_grammarlists: function(cont,err) { // May call cont several times!
+	    var ds=this.other_grammars_urls;
+	    var n=1+ds.length;
+	    function pair(dir) {
+		return function(grammar_list){cont(dir,grammar_list,n)}
+	    }
+	    function ignore_error(err) { console.log(err) }
+	    this.get_grammarlist(pair(this.grammars_url),err)
+	    for(var i in ds)
+		http_get_json(ds[i]+"grammars.cgi",pair(ds[i]),ignore_error);
+	},
+	pgf_call: function(cmd,args,cont,err) {
+	    var url=this.current_grammar_url+"?command="+cmd+encodeArgs(args)
+	    http_get_json(url,cont,err);
+	},
+	
+	get_languages: function(cont,err) {
+	    this.pgf_call("grammar",{},cont,err);
+	},
+	grammar_info: function(cont,err) {
+	    this.pgf_call("grammar",{},cont,err);
+	},
+	
+	get_random: function(args,cont,err) { // cat, limit
+	    args.random=Math.random(); // side effect!!
+	    this.pgf_call("random",args,cont,err);
+	},
+	linearize: function(args,cont,err) { // tree, to
+	    this.pgf_call("linearize",args,cont,err);
+	},
+	complete: function(args,cont,err) { // from, input, cat, limit
+	    this.pgf_call("complete",args,cont,err);
+	},
+	parse: function(args,cont,err) { // from, input, cat
+	    this.pgf_call("parse",args,cont,err);
+	},
+	translate: function(args,cont,err) { // from, input, cat, to
+	    this.pgf_call("translate",args,cont,err);
+	},
+	translategroup: function(args,cont,err) { // from, input, cat, to
+	    this.pgf_call("translategroup",args,cont,err);
+	},
+	browse: function(args,cont,err) { // id, format
+	    if(!args.format) args.format="json"; // sife effect!!
+	    this.pgf_call("browse",args,cont,err);
+	}
+    };
+    for(var o in options) server[o]=options[o];
+    if(server.grammar_list && server.grammar_list.length>0)
+	server.switch_grammar(server.grammar_list[0]);
+    return server;
+}
diff --git a/src/www/syntax-editor/js/support.js b/src/www/syntax-editor/js/support.js
new file mode 100644
index 000000000..e82f4fc9c
--- /dev/null
+++ b/src/www/syntax-editor/js/support.js
@@ -0,0 +1,329 @@
+/* --- Accessing document elements ------------------------------------------ */
+
+function element(id) {
+  return document.getElementById(id);
+}
+
+/* --- JavaScript tricks ---------------------------------------------------- */
+
+// To be able to use object methods that refer to "this" as callbacks
+// See section 3.3 of https://github.com/spencertipping/js-in-ten-minutes/raw/master/js-in-ten-minutes.pdf
+function bind(f, this_value) {
+    return function () {return f.apply (this_value, arguments)};
+};
+
+// Implement Array.isArray for older browsers that lack it.
+// https://developer.mozilla.org/en/JavaScript/Reference/Global_Objects/Array/isArray
+if(!Array.isArray) {
+    Array.isArray = function (arg) {
+        return Object.prototype.toString.call(arg) == '[object Array]';
+    };
+}
+
+/* --- JSONP ---------------------------------------------------------------- */
+
+// Inspired by the function jsonp from 
+//          http://www.west-wind.com/Weblog/posts/107136.aspx
+// See also http://niryariv.wordpress.com/2009/05/05/jsonp-quickly/
+//          http://en.wikipedia.org/wiki/JSONP
+function jsonp(url,callback)
+{                
+    if (url.indexOf("?") > -1)
+        url += "&jsonp=" 
+    else
+        url += "?jsonp=" 
+    url += callback;
+    //url += "&" + new Date().getTime().toString(); // prevent caching        
+    
+    var script = empty("script");        
+    script.setAttribute("src",url);
+    script.setAttribute("type","text/javascript");                
+    document.body.appendChild(script);
+}
+
+var json = {next:0};
+
+// Like jsonp, but instead of passing the name of the callback function, you 
+// pass the callback function directly, making it possible to use anonymous
+// functions.
+function jsonpf(url,callback,errorcallback)
+{
+    var name="callback"+(json.next++);
+    json[name]=function(x) { delete json[name]; callback(x); }
+    jsonp(url,"json."+name);
+}
+
+/* --- AJAX ----------------------------------------------------------------- */
+
+function GetXmlHttpObject(handler)
+{ 
+  var objXMLHttp=null
+  if (window.XMLHttpRequest)
+  {
+    // See http://www.w3.org/TR/XMLHttpRequest/
+    //     https://developer.mozilla.org/en/xmlhttprequest
+    objXMLHttp=new XMLHttpRequest()
+  }
+  else if (window.ActiveXObject)
+  {
+    objXMLHttp=new ActiveXObject("Microsoft.XMLHTTP")
+  }
+  return objXMLHttp
+}
+
+function ajax_http(method,url,body,callback,errorcallback) {
+    var http=GetXmlHttpObject()
+    if (!http) {
+	var errortext="Browser does not support HTTP Request";
+	if(errorcallback) errorcallback(errortext,500)
+	else alert(errortext)
+    }
+    else {
+	function statechange() {
+	    if (http.readyState==4 || http.readyState=="complete") {
+		if(http.status<300) callback(http.responseText,http.status);
+		else if(errorcallback)
+		    errorcallback(http.responseText,http.status,
+				  http.getResponseHeader("Content-Type"));
+		else alert("Request for "+url+" failed: "
+			   +http.status+" "+http.statusText);
+	    }
+	}
+	http.onreadystatechange=statechange;
+	http.open(method,url,true)
+	http.send(body)
+    }
+    return http
+}
+
+function ajax_http_get(url,callback,errorcallback) {
+    ajax_http("GET",url,null,callback,errorcallback)
+}
+
+function ajax_http_post(url,formdata,callback,errorcallback) {
+    ajax_http("POST",url,formdata,callback,errorcallback)
+    // See https://developer.mozilla.org/En/XMLHttpRequest/Using_XMLHttpRequest#Using_FormData_objects
+}
+
+// JSON via AJAX
+function ajax_http_get_json(url,cont,errorcallback) {
+    ajax_http_get(url,function(txt){cont(eval("("+txt+")"));}, errorcallback);
+}
+
+function sameOrigin(url) {
+    var a=empty("a");
+    a.href=url; // converts to an absolute URL
+    return hasPrefix(a.href,location.protocol+"//"+location.host+"/");
+}
+
+// Use AJAX when possible, fallback to JSONP
+function http_get_json(url,cont,errorcallback) {
+    if(sameOrigin(url)) ajax_http_get_json(url,cont,errorcallback);
+    else jsonpf(url,cont,errorcallback);
+}
+
+/* --- URL construction ----------------------------------------------------- */
+
+function encodeArgs(args) {
+    var q=""
+    for(var arg in args)
+	if(args[arg]!=undefined)
+	    q+="&"+arg+"="+encodeURIComponent(args[arg]);
+    return q;
+}
+
+/* --- HTML construction ---------------------------------------------------- */
+function text(s) { return document.createTextNode(s); }
+
+function node(tag,as,ds) {
+    var n=document.createElement(tag);
+    for(var a in as) n.setAttribute(a,as[a]);
+    if(ds) for(var i in ds) n.appendChild(ds[i]);
+    return n;
+}
+
+function empty(tag,name,value) {
+    var el=node(tag,{},[])
+    if(name && value) el.setAttribute(name,value);
+    return el;
+}
+
+function empty_id(tag,id) { return empty(tag,"id",id); }
+function empty_class(tag,cls) { return empty(tag,"class",cls); }
+
+function div_id(id,cs) { return node("div",{id:id},cs); }
+function span_id(id) { return empty_id("span",id); }
+
+function wrap(tag,contents) {
+    return node(tag,{},Array.isArray(contents) ? contents : [contents]);
+}
+
+function wrap_class(tag,cls,contents) {
+    return node(tag,{"class":cls},
+		contents ? Array.isArray(contents) ? 
+		contents : [contents] : [])
+}
+
+function span_class(cls,contents) { return wrap_class("span",cls,contents); }
+function div_class(cls,contents)  { return wrap_class("div",cls,contents); }
+
+function p(contents) { return wrap("p",contents); }
+function dt(contents) { return wrap("dt",contents); }
+function dd(contents) { return wrap("dd",contents); }
+function li(contents) { return wrap("li",contents); }
+
+function th(contents) { return wrap("th",contents); }
+function td(contents) { return wrap("td",contents); }
+
+function tr(cells)    { return wrap("tr",cells); }
+
+function button(label,action,key) {
+    var el=node("input",{"type":"button","value":label},[]);
+    if(typeof action=="string") el.setAttribute("onclick",action);
+    else el.onclick=action;
+    if(key) el.setAttribute("accesskey",key);
+    return el;
+}
+
+function option(label,value) {
+    return node("option",{"value":value},[text(label)]);
+}
+
+function hidden(name,value) {
+    return node("input",{type:"hidden",name:name,value:value},[])
+}
+
+function tda(cs) { return node("td",{},cs); }
+
+function img(src) { return empty("img","src",src); }
+
+/* --- Document modification ------------------------------------------------ */
+
+function clear(el) { replaceInnerHTML(el,""); }
+function replaceInnerHTML(el,html) { if(el) el.innerHTML=html; }
+function replaceChildren(el,newchild) { clear(el); el.appendChild(newchild); }
+
+function appendChildren(el,ds) {
+    for(var i in ds) el.appendChild(ds[i]);
+    return el;
+}
+
+function insertFirst(parent,child) {
+    parent.insertBefore(child,parent.firstChild);
+}
+
+function insertBefore(el,ref) { ref.parentNode.insertBefore(el,ref); }
+
+function insertAfter(el,ref) {
+    ref.parentNode.insertBefore(el,ref.nextSibling);
+}
+
+/* --- Debug ---------------------------------------------------------------- */
+
+function debug(s) {
+    var d=element("debug");
+    if(d) d.appendChild(text(s+"\n"))
+}
+
+function show_props(obj, objName) {
+   var result = "";
+   for (var i in obj) {
+      result += objName + "." + i + " = " + obj[i] + "<br>";
+   }
+   return result;
+}
+
+function field_names(obj) {
+   var result = "";
+   for (var i in obj) {
+      result += " " + i;
+   }
+   return result;
+}
+
+/* --- Data manipulation ---------------------------------------------------- */
+function swap(a,i,j) { // Note: this doesn't work on strings.
+  var tmp=a[i];
+  a[i]=a[j];
+  a[j]=tmp;
+  return a;
+}
+
+function sort(a) {
+// https://developer.mozilla.org/en/Core_JavaScript_1.5_Reference/Global_Objects/Array/sort
+  return a.sort();
+  /* // Note: this doesn't work on strings.
+  for(var i=0;i<a.length-1;i++) {
+    var min=i;
+    for(var j=i+1;j<a.length;j++)
+      if(a[j]<a[min]) min=j;
+    if(min!=i) swap(a,i,min);
+  }
+  return a;
+  */
+}
+
+function filter(p,xs) {
+  var ys=[];
+  for(var i=0;i<xs.length;i++)
+    if(p(xs[i])) ys[ys.length]=xs[i];
+  return ys;
+}
+
+function implode(cs) { // array of strings to string
+  /*
+  var s="";
+  for(var i=0;i<cs.length;i++)
+    s+=cs[i];
+  return s;
+  */
+  return cs.join("");
+}
+
+function hasPrefix(s,pre) { return s.substr(0,pre.length)==pre; }
+
+function commonPrefix(s1,s2) {
+    for(var i=0;i<s1.length && i<s2.length && s1[i]==s2[i];i++);
+    return s1.substr(0,i);
+}
+
+/*
+function all(p,xs) {
+  for(var i=0;i<xs.length;i++)
+    if(!p(xs[i])) return false;
+  return true;
+}
+*/
+
+function map(f,xs) {
+  var ys=[];
+  for(var i=0;i<xs.length;i++) ys[i]=f(xs[i]);
+  return ys;
+}
+
+// map in continuation passing style 
+function mapc(f,xs,cont) { mapc_from(f,xs,0,[],cont); }
+
+function mapc_from(f,xs,i,ys,cont) {
+  if(i<xs.length)
+    f(xs[i],function(y){ys[i]=y;mapc_from(f,xs,i+1,ys,cont)});
+  else
+    cont(ys);
+}
+
+function overlaps(as,bs) {
+    for(var i=0;i<as.length;i++)
+	if(elem(as[i],bs)) return true;
+    return false;
+}
+
+function elem(a,as) {
+    for(var i=0;i<as.length;i++)
+	if(a==as[i]) return true;
+    return false;
+}
+
+function shuffle(a) {
+    for(i=0;i<a.length;i++) swap(a,i,Math.floor(Math.random()*a.length))
+    return a;
+}
diff --git a/src/www/syntax-editor/ui/style.css b/src/www/syntax-editor/ui/style.css
new file mode 100644
index 000000000..f4f29d040
--- /dev/null
+++ b/src/www/syntax-editor/ui/style.css
@@ -0,0 +1,64 @@
+body {
+    background: #ccc url("http://cloud.grammaticalframework.org/minibar/brushed-metal.png");
+}
+
+#tree
+{
+  white-space:pre;
+  font-family: monospace;
+  background: rgba(238, 238, 238, 0.6);
+  padding:0.5em;
+  margin:0.5em 0;
+  }
+
+#tree .node
+{
+  margin: 0.4em 0 0.4em 1.5em;
+  }
+
+#tree .node a
+{ 
+  cursor: pointer;
+  }
+#tree .node a:hover
+{ 
+  text-decoration: underline;
+  }
+#tree .node a.current
+{ 
+  font-weight: bold;
+  }
+
+#linearisations
+{
+  background: rgba(170, 170, 170, 0.5);
+  padding:0.5em;
+  margin:0.5em 0;
+  }
+#linearisations div
+{
+  padding:0.2em;
+  }
+#linearisations .lang
+{
+  display: inline-block;
+  margin-right: 0.5em;
+  width: 3em;
+  font-weight: bold;
+  text-align: center;
+  }
+#linearisations .lin
+{
+  }
+
+.refinement
+{ 
+  margin: 0 0.1em;
+  display: inline-block;
+  cursor: pointer;
+  border: 1px solid;
+  padding: 0.2em;
+  font: 0.9em sans-serif;
+  background: white;
+  }
+
