gfse: added grammar cloning

src/editor/simple/TODO

@@ -7,7 +7,7 @@
 + Apply function alpha conversion in concrete syntax
 + Change lhs of lins when function type is changed
 
-- Allow languages other than the ones in the given list to be added
++ Allow languages other than the ones in the given list to be added
 + Export as plain text
 + Allow definitions to be reordered
 
@@ -24,6 +24,10 @@
 -    Easy access to compute_concrete from the editor
 -    Instead of starting with an empty grammar, start a new grammar by copying
      an example.
++ Cloning grammars
+- Allow grammars to contain a resoure module. Create the resource module by
+ factoring out common parts of the concrete syntaxes.
+- Integrate example-based concrete syntax construction (using Ramona's tool)
 
 + compile only the uploaded grammar even if other grammars are present
 + 'flags startcat' is needed for grammars with only one category (since the
@@ -34,3 +38,4 @@
 
 + Bug! The startcat menu shows the first category by default, but the startcat
   flag is actually not set until a selection is made from the menu.
+

src/editor/simple/editor.js

@@ -37,12 +37,15 @@ function draw_grammar_list() {
     editor.appendChild(home)
     var gs=ul([]);
     function del(i) { return function () { delete_grammar(i); } }
+    function clone(i) { return function (g,b) { clone_grammar(i); } }
     for(var i=0;i<local.count;i++) {
 	var grammar=local.get(i,null);
 	if(grammar && grammar.basename) {
 	    var link=a(jsurl("open_grammar("+i+")"),[text(grammar.basename)]);
 	    gs.appendChild(
-		li([deletable(del(i),link,"Delete this grammar")]))
+		node("li",{"class":"extensible"},
+		     [deletable(del(i),link,"Delete this grammar"),
+		      more(grammar,clone(i),"Clone this grammar")]))
 	}
     }
     if(local.get("count",null)==null)
@@ -80,6 +83,13 @@ function delete_grammar(i) {
     }
 }
 
+function clone_grammar(i) {
+    var old=local.get(i);
+    var g={basename:old.basename,abstract:old.abstract,concretes:old.concretes}
+    save_grammar(g);
+    draw_grammar_list();
+}
+
 function open_grammar(i) {
     var g=local.get(i);
     g.index=i;