summaryrefslogtreecommitdiff
path: root/src/www/gfse
diff options
context:
space:
mode:
authorhallgren <hallgren@chalmers.se>2012-02-21 16:58:18 +0000
committerhallgren <hallgren@chalmers.se>2012-02-21 16:58:18 +0000
commit2eddc116e676b249d300e930263255bfab057622 (patch)
tree83102f3dc9445701ffeb3444722558b5398ac6a6 /src/www/gfse
parent5403e31264f25c5a2d93d978a6a2ed66eb9a1929 (diff)
gfse: edit abstract syntax in text mode with instant syntax error reporting
This is an experimental feature. It requires server support for parsing and is thus not available while offline, unlike most other editing functionality.
Diffstat (limited to 'src/www/gfse')
-rw-r--r--src/www/gfse/cloud2.js6
-rw-r--r--src/www/gfse/editor.js61
2 files changed, 66 insertions, 1 deletions
diff --git a/src/www/gfse/cloud2.js b/src/www/gfse/cloud2.js
index 8d33315bd..02af9d91a 100644
--- a/src/www/gfse/cloud2.js
+++ b/src/www/gfse/cloud2.js
@@ -193,6 +193,12 @@ function gfshell(cmd,cont) {
})
}
+// Check the syntax of a source module
+function check_module(path,source,cont) {
+ var enc=encodeURIComponent;
+ http_get_json("/parse?"+enc(path)+"="+enc(source),cont)
+}
+
// Check the syntax of an expression
function check_exp(s,cont) {
function check(gf_message) {
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js
index b630f69ab..60abf2142 100644
--- a/src/www/gfse/editor.js
+++ b/src/www/gfse/editor.js
@@ -453,7 +453,7 @@ function draw_abstract(g) {
timestamp(g.abstract);
save_grammar(g);
}
- return div_id("file",
+ var file=div_id("file",
[kw("abstract "),ident(g.basename),sep(" = "),
draw_timestamp(g.abstract),
draw_extends(g),
@@ -462,6 +462,65 @@ function draw_abstract(g) {
indent(draw_cats(g))]),
extensible([kw_fun,
indent_sortable(draw_funs(g),sort_funs)])])]);
+ if(navigator.onLine) {
+ var mode_button=text_mode(g,file);
+ insertBefore(mode_button,file.firstChild)
+ }
+ return file;
+}
+
+function text_mode(g,file) {
+ var path=g.basename+".gf"
+ function switch_to_guided_mode() {
+ edit_grammar(g); // !!
+ }
+ function store_parsed(parse_results) {
+ var dst=compiler_output;
+ var msg=parse_results[path];
+ if(dst) dst.innerHTML=""
+ console.log(msg)
+ if(dst && msg.error)
+ dst.appendChild(span_class("error_message",
+ text(msg.location+": "+msg.error)))
+ else if(dst && msg.parsed)
+ dst.innerHTML=
+ "Accepted by GF, but not by this editor ("+msg.parsed+")"
+ else if(msg.converted) {
+ var gnew=msg.converted;
+ g.abstract=gnew.abstract;
+ g.extends=gnew.extends;
+ timestamp(g.abstract);
+ save_grammar(g);
+ }
+ else if(dst) dst.innerHTML="unexpected parse result";
+ }
+ var last_source=show_abstract(g);
+ function parse(source) {
+ if(source!=last_source) {
+ if(navigator.onLine) {
+ //compiler_output.innerHTML="";
+ last_source=source;
+ check_module(path,source,store_parsed)
+ }
+ else if(compiler_output)
+ compiler_output.innerHTML="Offline, edits will not be saved"
+ }
+ }
+ function switch_to_text_mode() {
+ var ta=node("textarea",{class:"text_mode",rows:25,cols:80},
+ [text(show_abstract(g))])
+ var timeout;
+ ta.onkeyup=function() {
+ if(timeout) clearTimeout(timeout);
+ timeout=setTimeout(function(){parse(ta.value)},400)
+ }
+ var mode_button=div_class("right",[button("Guided mode",switch_to_guided_mode)])
+ file.innerHTML="";
+ appendChildren(file,[mode_button,ta])
+ ta.focus();
+ }
+ var mode_button=div_class("right",[button("Text mode",switch_to_text_mode)])
+ return mode_button;
}
function add_cat(g,el) {