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/editor/simple/cloud2.js | 159 -------------------------------------------- 1 file changed, 159 deletions(-) delete mode 100644 src/editor/simple/cloud2.js (limited to 'src/editor/simple/cloud2.js') diff --git a/src/editor/simple/cloud2.js b/src/editor/simple/cloud2.js deleted file mode 100644 index e32749dc1..000000000 --- a/src/editor/simple/cloud2.js +++ /dev/null @@ -1,159 +0,0 @@ - -function with_dir(cont) { - var dir=local.get("dir",""); - if(/^\/tmp\//.test(dir)) cont(dir); - else ajax_http_get("/new", - function(dir) { - local.put("dir",dir); - cont(dir); - }); -} - -function remove_cloud_grammar(g) { - var dir=local.get("dir") - if(dir && g.unique_name) { - var path=g.unique_name+".json" - gfcloud("rm",{file:path},debug); - } -} - -// Upload the grammar to the server and check it for errors -function upload(g) { - function upload2(dir) { - var form=node("form",{method:"post",action:"/cloud"}, - [hidden("dir",dir),hidden("command","make"), - hidden(g.basename+".gf",show_abstract(g))]) - var files = [g.basename+".gf"] - for(var i in g.concretes) { - var cname=g.basename+g.concretes[i].langcode+".gf"; - files.push(cname); - form.appendChild(hidden(cname, - show_concrete(g.basename)(g.concretes[i]))); - } - editor.appendChild(form); - form.submit(); - form.parentNode.removeChild(form); - } - - function upload3(message) { if(message) alert(message); } - - with_dir(upload2) -} - -// Upload the grammar to store it in the cloud -function upload_json(cont) { - function upload3(resptext,status) { - local.put("json_uploaded",Date.now()); - //debug("Upload complete") - if(cont) cont(); - else { - var sharing=element("sharing"); - if(sharing) sharing.innerHTML=resptext; - } - } - function upload2(dir) { - var prefix=dir.substr(10)+"-" // skip "/tmp/gfse." - //debug("New form data"); - //var form=new FormData(); // !!! Doesn't work on Android 2.2! - var form={dir:dir}; - //debug("Preparing form data"); - for(var i=0;i