Syntax editor: update to use common js files

5 files changed, 0 insertions, 1081 deletions

diff --git a/src/www/syntax-editor/js/ast.js b/src/www/syntax-editor/js/ast.js
deleted file mode 100644
index 633bdc2b6..000000000
--- a/src/www/syntax-editor/js/ast.js
+++ /dev/null
@@ -1,204 +0,0 @@
-/* --- 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 ASTNode(data) {
-    for(var d in data) this[d]=data[d];
-    this.children = [];
-    // if (children != undefined)
-    //     for (c in children) {
-    //         this.children.push( new ASTNode(children[c]) );
-    //     }
-    this.hasChildren = function(){
-        return this.children.length > 0;
-    }
-
-    // generic HOF for traversing tree
-    this.traverse = function(f) {
-        function visit(node) {
-            f(node);
-            for (i in node.children) {
-                visit(node.children[i]);
-            }
-        }
-        visit(this);
-    }
-    
-}
-
-function AST(fun, cat) {
-
-    // local helper function for building ASTNodes
-    newNode = function(fun, cat) {
-        return new ASTNode({
-            "fun": fun,
-            "cat": cat,
-            "children": []
-        });
-    }
-
-    this.root = newNode(fun, cat);
-    
-    this.current = new NodeID(); // current id in tree
-
-    this.getFun = function() {
-        return this.find(this.current).fun;
-    }
-    this.setFun = function(f) {
-        this.find(this.current).fun = f;
-    }
-    this.getCat = function() {
-        return this.find(this.current).cat;
-    }
-    this.setCat = function(c) {
-        this.find(this.current).cat = c;
-    }
-
-
-    // Add a single fun at current node
-    this.add = function(fun, cat) {
-        this._add(this.current, newNode(fun,cat));
-    }
-
-    // add node as child of id
-    this._add = function(id, node) {
-        var x = this.find(id);
-        x.children.push(node);
-    }
-
-    // Set entire subtree at current node
-    this.setSubtree = function(node) {
-        this._setSubtree(this.current, node);
-    }
-    
-    // set tree at given id to 
-    this._setSubtree = function(id, node) {
-        var x = this.find(id);
-        for (var n in node) x[n] = node[n];
-
-        x.traverse(function(node){
-            if (!node.children) node.children=[];
-            // TODO: this doesn't work!
-            //node = new ASTNode(node);
-        })
-    }
-
-    // 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;
-    }
-    
-    // Clear children of current node
-    this.removeChildren = function() {
-        this.find(this.current).children = [];
-    }
-
-    // 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.find(id);
-
-            // first check children
-            for (i in node.children) {
-                var child = node.children[i];
-                if (!child.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);
-    }
-
-    // generic HOF for traversing tree
-    // this.traverse = function(f) {
-    //     this.root.traverse(f);
-    // }
-    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.root);
-    }
-
-    // Return tree as string
-    this.toString = function() {
-        var s = "";
-        function visit(node) {
-            s += node.fun ? node.fun : "?" ;
-//            if (!node.hasChildren())
-            if (node.children.length == 0)
-                return;
-            for (i in node.children) {
-                s += " (";
-                visit(node.children[i]);
-                s += ")";
-            }
-        }
-        visit(this.root);
-        return s;
-    }
-
-}
-
diff --git a/src/www/syntax-editor/js/editor.js b/src/www/syntax-editor/js/editor.js
deleted file mode 100644
index 1f6a374b5..000000000
--- a/src/www/syntax-editor/js/editor.js
+++ /dev/null
@@ -1,295 +0,0 @@
-
-/* --- 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);
-
-}
-
-Editor.prototype.get_grammar_constructors=function(callback) {
-    var t = this;
-    var args = {
-        format: "json"
-    };
-    var cont = function(data){
-        t.grammar_constructors = data;
-        if (callback) callback();
-    };
-    var err = function(data){
-        alert("Error");
-    };
-    t.server.browse(args, cont, err);
-}
-
-/* --- 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;
-        get_grammar_constructors(bind(start_fresh,this));
-    }
-}
-
-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) {
-    var t = this;
-    if (cat == undefined)
-        cat = t.ast.getCat();
-    var args = {
-        id: cat,
-        format: "json"
-    };
-    var cont = function(data){
-        clear(t.ui.refinements);
-        for (pi in data.producers) {
-            var opt = span_class("refinement", text(data.producers[pi]));
-            opt.onclick = bind(function(){ t.select_refinement(this.innerHTML) }, opt);
-            t.ui.refinements.appendChild(opt);
-        }
-    };
-    var err = function(data){
-        clear(t.ui.refinements);
-        alert("Error");
-    };
-    t.server.browse(args, cont, err);
-}
-
-Editor.prototype.select_refinement=function(fun) {
-    with (this) {
-        ui.refinements.innerHTML = "...";
-        ast.removeChildren();
-        ast.setFun(fun);
-        var args = {
-            id: fun,
-            format: "json"
-        };
-        var err = function(data){
-            alert("Error");
-        };
-        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]);
-            }
-        }
-        
-        // Update ui
-        redraw_tree();
-        update_linearisation();
-
-        // Select next hole & get its refinements
-        ast.toNextHole();
-        update_current_node();
-    }
-}
-
-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.fun) ? node.fun : "?") + " : " +
-            ((node.cat) ? node.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.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);
-                }
-            }
-        });
-    }
-}
-
-// 
-Editor.prototype.delete_refinement = function() {
-    var t = this;
-    t.ast.removeChildren();
-    t.ast.setFun(null);
-    t.redraw_tree();
-//    t.get_refinements();
-}
-
-// Generate random subtree from current node
-Editor.prototype.generate_random = function() {
-    var t = this;
-    t.ui.refinements.innerHTML = "...";
-    t.ast.removeChildren();
-    var args = {
-        cat: t.ast.getCat(),
-        limit: 1
-    };
-    if (!args.cat) {
-        alert("Missing category at current node");
-        return;
-    }
-    var cont = function(data){
-        var tree = data[0].tree;
-        t.import_ast(tree);
-    };
-    var err = function(data){
-        alert("Error");
-    };
-    server.get_random(args, cont, err);
-}
-
-// Import AST from string representation
-Editor.prototype.import_ast = function(abstr) {
-    var t = this;
-    var args = {
-        tree: abstr
-    };
-    var cont = function(tree){
-        // Build tree of just fun, then populate with cats
-        t.ast.setSubtree(tree);
-        t.ast.traverse(function(node){
-            var info = t.lookup_fun(node.fun);
-            node.cat = info.cat;
-        });
-        t.redraw_tree();
-        t.update_linearisation();
-    };
-    server.pgf_call("abstrjson", args, cont);
-}
-
-// Look up information for a function, hopefully from cache
-Editor.prototype.lookup_fun = function(fun) {
-    var t = this;
-    var def = t.grammar_constructors.funs[fun].def;
-    var ix = def.lastIndexOf(" ");
-    var cat = def.substr(ix).trim();
-    return {
-        cat: cat
-    }
-}
-
diff --git a/src/www/syntax-editor/js/editor_menu.js b/src/www/syntax-editor/js/editor_menu.js
deleted file mode 100644
index ded47f54e..000000000
--- a/src/www/syntax-editor/js/editor_menu.js
+++ /dev/null
@@ -1,173 +0,0 @@
-/* --- 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_toggle: button("...", function(){
-            var sel = t.ui.to_menu;
-            if (sel.classList.contains("hidden"))
-                sel.classList.remove("hidden")
-            else
-                sel.classList.add("hidden")
-        }),
-        to_menu: node("select",{
-            id: "to_menu",
-            multiple: "multiple",
-            class: "hidden"
-        }),
-        clear_button: button("Clear", function(){
-            t.editor.delete_refinement();
-        }),
-        random_button: button("Random", function(){
-            t.editor.generate_random();
-        }),
-    };
-    with(this.ui) {
-	appendChildren(this.container, [text(" Startcat: "),startcat_menu]);
-        appendChildren(this.container, [text(" To: "), to_toggle, to_menu]);
-        appendChildren(this.container, [clear_button, random_button]);
-        // appendChildren(this.container, [clear_button]);
-        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 () {
-    this.editor.languages = new Array();
-    for (i in this.ui.to_menu.options) {
-        var opt = this.ui.to_menu.options[i];
-        if (opt.selected)
-            this.editor.languages.push(opt.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
deleted file mode 100644
index 6fe23b13e..000000000
--- a/src/www/syntax-editor/js/pgf_online.js
+++ /dev/null
@@ -1,80 +0,0 @@
-
-/* --- 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
deleted file mode 100644
index e82f4fc9c..000000000
--- a/src/www/syntax-editor/js/support.js
+++ /dev/null
@@ -1,329 +0,0 @@
-/* --- 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;
-}