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/www/minibar/support.js | 300 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) create mode 100644 src/www/minibar/support.js (limited to 'src/www/minibar/support.js') diff --git a/src/www/minibar/support.js b/src/www/minibar/support.js new file mode 100644 index 000000000..c65c1a389 --- /dev/null +++ b/src/www/minibar/support.js @@ -0,0 +1,300 @@ +/* --- 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