From 44d1a5a9f71b03d9aceeccd760a63fcdc45f8bad Mon Sep 17 00:00:00 2001 From: hallgren Date: Wed, 12 Oct 2011 17:03:54 +0000 Subject: Improvements of "gf -server" mode and related setup "gf -server" mode now contains everything needed to run the minibar and the grammar editor (including example-based grammar writing). The Setup.hs script installs the required files where gf -server can find them. These files have been moved to a new directory: src/www. The separate server program pgf-http is now obsolete. --- src/runtime/javascript/minibar/support.js | 300 ------------------------------ 1 file changed, 300 deletions(-) delete mode 100644 src/runtime/javascript/minibar/support.js (limited to 'src/runtime/javascript/minibar/support.js') diff --git a/src/runtime/javascript/minibar/support.js b/src/runtime/javascript/minibar/support.js deleted file mode 100644 index c65c1a389..000000000 --- a/src/runtime/javascript/minibar/support.js +++ /dev/null @@ -1,300 +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)}; -}; - -/* --- 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/JSON#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) -{ - 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 { - var statechange=function() { - if (http.readyState==4 || http.readyState=="complete") { - if(http.status<300) callback(http.responseText,http.status); - else if(errorcallback) errorcallback(http.responseText,http.status); - 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) { - ajax_http_get(url,function(txt) { cont(eval("("+txt+")")); }); -} - -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) { - if(sameOrigin(url)) ajax_http_get_json(url,cont); - else jsonpf(url,cont); -} - -/* --- 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]); - 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) { return empty_id("div",id); } -function span_id(id) { return empty_id("span",id); } - -function wrap(tag,contents) { return node(tag,{},[contents]); } - -function wrap_class(tag,cls,contents) { - var el=empty_class(tag,cls); - if(contents) el.appendChild(contents); - return el; -} - -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 li(contents) { return wrap("li",contents); } - -function th(contents) { return wrap("th",contents); } -function td(contents) { return wrap("td",contents); } - -function tr(cells) { return node("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 appendChildren(el,ds) { - for(var i in ds) el.appendChild(ds[i]); - return el; -} - -function insertFirst(parent,child) { - parent.insertBefore(child,parent.firstChild); -} - -function tda(cs) { return node("td",{},cs); } - -function img(src) { return empty("img","src",src); } - -/* --- 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] + "
"; - } - 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