gfse: some correctness checks for concrete syntax

The editor now calls the GF server to check the syntax of expressions that
are part of concrete syntax (except for parameter types).
This is currently done by using the cc command of the GF shell, which puts
some unnecessary restricitons on operation definitions...

src/editor/simple/about.html

@@ -116,7 +116,8 @@ At the moment, the concrete syntax for a language <var>L</var> is limited to
   <li><em>linearizations</em> for the functions in the abstract syntax,
   <li><em>parameter type definitions</em>,
   <var>P</var> = <var>C<sub>1</sub></var> | ... |<var>C<sub>n</sub></var>,
-  <li>and <em>operation definitions</em>, <var>op</var> = <var>expr</var>.
+  <li>and <em>operation definitions</em>, <var>op</var> = <var>expr</var>,
+   <var>op</var> : <var>type</var> = <var>expr</var>,
 </ul>
 
 Available editing operations:
@@ -146,8 +147,11 @@ Also,
 
 Error checks:
 <ul>
-  <li>The RHSs in the concrete syntax are not checked for errors. Arbitrary
+  <li>The RHSs in the concrete syntax are checked
-  strings can be entered.
+  for syntactic correctness by the editor as they are entered.
+  (TODO: the syntax of parameter types is not check at the moment.)
+  <li>Duplicated definitions are highlighted. Checks for other
+  semantic errors are delayed until the grammar is compiled.
 </ul>
 
 <h3>Compiling and testing grammars</h3>
@@ -164,7 +168,7 @@ cloud</h3>
 
 While the editor normally stores grammars locally in the browser, it is also
 possible to store grammars in the cloud.  Grammars can be stored in the cloud
-just for backup, or to accessed them from multiple devices.
+just for backup, or to make them accessible from multiple devices.
 
 <p>
 There is no automatic synchronization between local grammars and the cloud.
@@ -197,14 +201,13 @@ devices, but not recommended for sharing grammars between multiple users.
 
 <p>
 Also <strong>note</strong> that each grammar is assigned a unique identity
-when it is created. Renaming a grammar does not change its identity. This means
+when it is first created. Renaming a grammar does not change its identity.
-that name changes are propagated between devices like other changes.
+This means that name changes are propagated between devices like other changes.
 
 <h3>Future work</h3>
 
 This prototype gives an idea of how a web based GF grammar editor could work.
-While this editor is implemented in JavaScript and runs entirely in the
+While this editor is implemented in JavaScript and runs in the web browser,
-web browser,
 we do not expect to create a full implementation of GF that runs in the
 web browser, but let the editor communicate with a server running GF.
 <p>
@@ -214,7 +217,7 @@ to do proper error checking and make more of the existing GF shell functionality
 accessible directly from the editor.
 <p>
 The current grammar cloud service is very primitive. In particular, it is not
-suitable for multiple users developing  a grammar in collaboration.
+suitable for multiple users developing a grammar in collaboration.
 
 <h3>Related documents</h3>
 <ul>
@@ -225,7 +228,7 @@ suitable for multiple users developing  a grammar in collaboration.
 
 <hr>
 <div class=modtime><small>
-<!-- hhmts start --> Last modified: Tue Jul 26 17:01:22 CEST 2011 <!-- hhmts end -->
+<!-- hhmts start --> Last modified: Fri Jul 29 17:44:00 CEST 2011 <!-- hhmts end -->
   </small></div>
 <address>
 <a href="http://www.cse.chalmers.se/~hallgren/">TH</a>

src/editor/simple/cloud.js

@@ -136,6 +136,11 @@ function gfshell(cmd,cont) {
 
 // Check the syntax of an expression
 function check_exp(s,cont) {
-    // Not implemented yet!!
+    function check(gf_message) {
-    cont(null)
+	debug("cc "+s+" = "+gf_message);
+	cont(/parse error/.test(gf_message) ? "parse error" : null);
+    }
+    if(navigator.onLine)
+	ajax_http_get("upload.cgi?cc="+encodeURIComponent(s),check)
+    else cont(null)
 }

src/editor/simple/editor.js

@@ -671,39 +671,50 @@ function draw_oper(p,dp) {
     return node("span",{},[check(ident(p.name)),text(" "),text(p.rhs)]);
 }
 
+function check_oper(s,ok,err) {
+    var p=parse_oper(s);
+    function check2(msg) {
+	if(msg) err(msg);
+	else ok(p.ok)
+    }
+    if(p.ok) {
+	// Checking oper syntax by checking an expression with a local
+	// definition. Some valid opers will be rejected!!
+	var e=p.ok.name+" where { "+p.ok.name+" "+p.ok.rhs+" }";
+	check_exp(e,check2);
+    }
+    else
+	err(p.error);
+}
+
 function add_oper(g,ci,el) {
-    function add(s) {
+    function check(s,cont) {
-	var p=parse_oper(s);
+	function ok(oper) {
-	if(p.ok) {
+	    g.concretes[ci].opers.push(oper);
-	    g.concretes[ci].opers.push(p.ok);
 	    timestamp(g.concretes[ci]);
 	    reload_grammar(g);
-	    return null;
+	    cont(null);
 	}
-	else
+	check_oper(s,ok,cont)
-	    return p.error
     }
-    string_editor(el,"",add);
+    string_editor(el,"",check,true);
 }
 
 function edit_oper(ci,i) {
     return function (g,el) {
-	function replace(s) {
+	function check(s,cont) {
-	    var p=parse_oper(s);
+	    function ok(oper) {
-	    if(p.ok) {
+		g.concretes[ci].opers[i]=oper;
-		g.concretes[ci].opers[i]=p.ok;
 		timestamp(g.concretes[ci]);
 		reload_grammar(g);
-		return null;
+		cont(null);
 	    }
-	    else
+	    check_oper(s,ok,cont)
-		return p.error;
 	}
-	string_editor(el,show_oper(g.concretes[ci].opers[i]),replace);
+	string_editor(el,show_oper(g.concretes[ci].opers[i]),check,true);
     }
 }
 
-
 function delete_oper(g,ci,ix) {
     with(g.concretes[ci]) opers=delete_ix(opers,ix);
     timestamp(g.concretes[ci]);

src/editor/simple/upload.cgi

@@ -219,6 +219,13 @@ case "$REQUEST_METHOD" in
                 *) error400
 	     esac
 	     ;;
+	cc=*)
+	     # Just to check an expression for syntax errors
+	     exp=$(qparse "$QUERY_STRING" cc)
+	     ContentType="text/plain; charset=$charset"
+	     cgiheaders
+	     echo "cc $exp" | GF_RESTRICTED=True gf -run
+	     ;;
         *) error400
     esac
 esac