fake_ide: speak the new protocol

A new syntax for .fake files, allowing multi line phrases and
labeled script points (to go back to them).

Test 7 fails because of a bug in STM (in a very spaghetti-like script).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 407 insertions, 289 deletions

diff --git a/Makefile.build b/Makefile.build
index 902f84202..99ef062b9 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -543,7 +543,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
 
 $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) tools/fake_ide$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,unix)
+	$(HIDE)$(call bestocaml,,str unix)
 
 # votour: a small vo explorer (based on the checker)
 
diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
index bbaea7e7e..552636157 100644
--- a/test-suite/ide/undo001.fake
+++ b/test-suite/ide/undo001.fake
@@ -3,8 +3,8 @@
 #
 # Simple backtrack by 1 between two global definitions
 #
-INTERP Definition foo := 0.
-INTERP Definition bar := 1.
-REWIND 1
-INTERPRAW Check foo.
-INTERPRAW Fail Check bar.
+ADD here { Definition foo := 0. }
+ADD { Definition bar := 1. }
+EDIT_AT here
+QUERY { Check foo. }
+QUERY { Fail Check bar. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index b855b6ea7..5284c5d3a 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,8 +3,8 @@
 #
 # Simple backtrack by 2 before two global definitions
 #
-INTERP Definition foo := 0.
-INTERP Definition bar := 1.
-REWIND 2
-INTERPRAW Fail Check foo.
-INTERPRAW Fail Check bar.
+ADD { Definition foo := 0. }
+ADD { Definition bar := 1. }
+EDIT_AT initial
+QUERY { Fail Check foo. }
+QUERY { Fail Check bar. }
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
index 4c72e8dc7..907576276 100644
--- a/test-suite/ide/undo003.fake
+++ b/test-suite/ide/undo003.fake
@@ -3,6 +3,6 @@
 #
 # Simple backtrack by 0 should be a no-op
 #
-INTERP Definition foo := 0.
-REWIND 0
-INTERPRAW Check foo.
+ADD here { Definition foo := 0. }
+EDIT_AT here
+QUERY { Check foo. }
diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
index c2ddfb8cb..9029b03e2 100644
--- a/test-suite/ide/undo004.fake
+++ b/test-suite/ide/undo004.fake
@@ -3,12 +3,12 @@
 #
 # Undoing arbitrary commands, as first step
 #
-INTERP Theorem a : O=O.
-INTERP Ltac f x := x.
-REWIND 1
+ADD here { Theorem a : O=O. }
+ADD { Ltac f x := x. }
+EDIT_AT here
 # <replay>
-INTERP Ltac f x := x.
+ADD { Ltac f x := x. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
index 525b9f2a6..7e31c0b05 100644
--- a/test-suite/ide/undo005.fake
+++ b/test-suite/ide/undo005.fake
@@ -3,13 +3,13 @@
 #
 # Undoing arbitrary commands, as non-first step
 #
-INTERP Theorem b : O=O.
-INTERP assert True by trivial.
-INTERP Ltac g x := x.
+ADD { Theorem b : O=O. }
+ADD here { assert True by trivial. }
+ADD { Ltac g x := x. }
 # <replay>
-REWIND 1
+EDIT_AT here
 # <\replay>
-INTERP Ltac g x := x.
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { Ltac g x := x. }
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
index ed88bef51..cdfdee1b7 100644
--- a/test-suite/ide/undo006.fake
+++ b/test-suite/ide/undo006.fake
@@ -4,11 +4,11 @@
 # Undoing declarations, as first step
 # Was bugged in 8.1
 #
-INTERP Theorem c : O=O.
-INTERP Inductive T : Type := I.
-REWIND 1
+ADD here { Theorem c : O=O. }
+ADD { Inductive T : Type := I. }
+EDIT_AT here
 # <replay>
-INTERP Inductive T : Type := I.
+ADD { Inductive T : Type := I. }
 # <\replay>
-INTERP trivial.
-INTERP Qed.
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
index 87c06dbb3..770350fbd 100644
--- a/test-suite/ide/undo007.fake
+++ b/test-suite/ide/undo007.fake
@@ -4,14 +4,18 @@
 # Undoing declarations, as first step
 # new in 8.2
 #
-INTERP Theorem d : O=O.
-INTERP Definition e := O.
-INTERP Definition f := O.
-REWIND 1
-# <replay>
-INTERP Definition f := O.
-# <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
-INTERPRAW Check e.
+ADD { Theorem d : O=O. }
+ADD here { Definition e := O. }
+ADD { Definition f := O. }
+
+# This is a bug in Stm undo, e is lost from master
+EDIT_AT here
+ADD { Definition f := O. }
+
+ADD { assert True by trivial. }
+ADD { exact (eq_refl e). }
+ADD { Qed. }
+ADD { Stm PrintDag. }
+ADD { Stm Finish. }
+QUERY { Print d. }
+QUERY { Check e. }
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 1c46c1e87..72cab7a30 100644
--- a/test-suite/ide/undo008.fake
+++ b/test-suite/ide/undo008.fake
@@ -4,15 +4,15 @@
 # Undoing declarations, as non-first step
 # new in 8.2
 #
-INTERP Theorem h : O=O.
-INTERP assert True by trivial.
-INTERP Definition i := O.
-INTERP Definition j := O.
-REWIND 1
+ADD { Theorem h : O=O. }
+ADD { assert True by trivial. }
+ADD here { Definition i := O. }
+ADD { Definition j := O. }
+EDIT_AT here
 # <replay>
-INTERP Definition j := O.
+ADD { Definition j := O. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
-INTERPRAW Check i.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
+QUERY { Check i. }
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
index 47c77d23d..76f400ef0 100644
--- a/test-suite/ide/undo009.fake
+++ b/test-suite/ide/undo009.fake
@@ -4,17 +4,18 @@
 # Undoing declarations, interleaved with proof steps
 # new in 8.2 *)
 #
-INTERP Theorem k : O=O.
-INTERP assert True by trivial.
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
-REWIND 3
+ADD { Theorem k : O=O. }
+ADD here { assert True by trivial. }
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
+QUERY { Show. }
+EDIT_AT here
 # <replay>
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
index 4fe9df986..524416c32 100644
--- a/test-suite/ide/undo010.fake
+++ b/test-suite/ide/undo010.fake
@@ -4,25 +4,25 @@
 # Undoing declarations, interleaved with proof steps and commands *)
 # new in 8.2 *)
 #
-INTERP Theorem n : O=O.
-INTERP assert True by trivial.
-INTERP Definition o := O.
-INTERP Ltac h x := x.
-INTERP assert True by trivial.
-INTERP Focus.
-INTERP Definition p := O.
-REWIND 1
-REWIND 1
-REWIND 1
-REWIND 1
-REWIND 1
+ADD { Theorem n : O=O. }
+ADD s2 { assert True by trivial. }
+ADD s3 { Definition o := O. }
+ADD s4 { Ltac h x := x. }
+ADD s5 { assert True by trivial. }
+ADD s6 { Focus. }
+ADD { Definition p := O. }
+EDIT_AT s6
+EDIT_AT s5
+EDIT_AT s4
+EDIT_AT s3
+EDIT_AT s2
 # <replay>
-INTERP Definition o := O.
-INTERP Ltac h x := x.
-INTERP assert True by trivial.
-INTERP Focus.
-INTERP Definition p := O.
+ADD { Definition o := O. }
+ADD { Ltac h x := x. }
+ADD { assert True by trivial. } 
+ADD { Focus. }
+ADD { Definition p := O. }
 # </replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
index cc85a764b..0be439b27 100644
--- a/test-suite/ide/undo011.fake
+++ b/test-suite/ide/undo011.fake
@@ -4,29 +4,31 @@
 # Bug 2082
 # Broken due to proof engine rewriting
 #
-INTERP Variable A : Prop.
-INTERP Variable B : Prop.
-INTERP Axiom OR : A \/ B.
-INTERP Lemma MyLemma2 : True.
-INTERP proof.
-INTERP per cases of (A \/ B) by OR.
-INTERP suppose A.
-INTERP     then (1 = 1).
-INTERP     then H1 : thesis.
-INTERP     thus thesis by H1.
-INTERP suppose B.
-REWIND 1
+ADD { Variable A : Prop. }
+ADD { Variable B : Prop. }
+ADD { Axiom OR : A \/ B. }
+ADD { Lemma MyLemma2 : True. }
+ADD { proof. }
+ADD { per cases of (A \/ B) by OR. }
+ADD { suppose A. }
+ADD {     then (1 = 1). }
+ADD there {     then H1 : thesis. }
+ADD here {     thus thesis by H1. }
+ADD { suppose B. }
+QUERY { Show. }
+EDIT_AT here
 # <replay>
-INTERP suppose B.
+ADD { suppose B. }
 # </replay>
-REWIND 2
+EDIT_AT there
 # <replay>
-INTERP     thus thesis by H1.
-INTERP suppose B.
+ADD {    thus thesis by H1. }
+ADD { suppose B. }
 # </replay>
-INTERP    then (1 = 1).
-INTERP    then H2 : thesis.
-INTERP    thus thesis by H2.
-INTERP end cases.
-INTERP end proof.
-INTERP Qed.
+QUERY { Show. }
+ADD {    then (1 = 1). }
+ADD {    then H2 : thesis. }
+ADD {    thus thesis by H2. }
+ADD { end cases. } 
+ADD { end proof. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
index 49169eba8..b3d1c6d53 100644
--- a/test-suite/ide/undo012.fake
+++ b/test-suite/ide/undo012.fake
@@ -2,25 +2,25 @@
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
-# First, undoing the whole
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-REWIND 1
-# We should now be just before aa, without opened proofs
-INTERPRAW Fail idtac.
-INTERPRAW Fail Check aa.
-INTERPRAW Check bb.
-INTERPRAW Check cc.
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+ADD { Qed. }
+QUERY { Show. }
+ADD here { apply H. }
+ADD { Qed. }
+EDIT_AT here
+# We should now be just before the Qed.
+QUERY { Fail Check aa. }
+QUERY { Check bb. }
+QUERY { Check cc. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index 389da2765..f44156aa3 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -2,27 +2,26 @@
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
-# Second, trigger the full undo of an inner proof
+# Second, trigger the undo of an inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-INTERP Qed.
-INTERP apply H.
-REWIND 2
-# We should now be just before "Lemma cc"
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD here { destruct H. }
+ADD { Qed. }
+ADD { apply H. }
+EDIT_AT here
 # <replay>
-INTERP Qed.
-INTERP apply H.
+ADD { Qed. }
+ADD { apply H. }
 # </replay>
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index 5224b5045..6d58b061e 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -4,23 +4,23 @@
 # Test backtracking in presence of nested proofs
 # Third, undo inside an inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 1
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD here { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP destruct H.
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index 32e46ec9a..ac17985aa 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -4,26 +4,26 @@
 # Test backtracking in presence of nested proofs
 # Fourth, undo from an inner proof to a above proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 4
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD here { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index a188e31b1..bdb81ecd9 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -4,29 +4,28 @@
 # Test backtracking in presence of nested proofs
 # Fifth, undo from an inner proof to a previous inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 6
-# We should be just before "Lemma bb"
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD here { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
index 232360e9d..37423dc72 100644
--- a/test-suite/ide/undo017.fake
+++ b/test-suite/ide/undo017.fake
@@ -3,11 +3,11 @@
 #
 # bug #2569 : Undoing inside modules
 #
-INTERP Module M.
-INTERP Definition x := 0.
-INTERP End M.
-REWIND 1
+ADD { Module M. }
+ADD here { Definition x := 0. }
+ADD { End M. }
+EDIT_AT here
 # <replay>
-INTERP End M.
+ADD { End M. }
 # </replay>
-INTERPRAW Check M.x.
+QUERY { Check M.x. }
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
index ef0945ab5..11091bfa6 100644
--- a/test-suite/ide/undo018.fake
+++ b/test-suite/ide/undo018.fake
@@ -3,11 +3,11 @@
 #
 # bug #2569 : Undoing inside section
 #
-INTERP Section M.
-INTERP Definition x := 0.
-INTERP End M.
-REWIND 1
+ADD { Section M. }
+ADD here { Definition x := 0. }
+ADD { End M. }
+EDIT_AT here
 # <replay>
-INTERP End M.
+ADD { End M. }
 # </replay>
-INTERPRAW Check x.
+QUERY { Check x. }
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
index 70e70d7e4..5df49ebbb 100644
--- a/test-suite/ide/undo019.fake
+++ b/test-suite/ide/undo019.fake
@@ -3,12 +3,12 @@
 #
 # bug #2569 : Undoing a focused subproof
 #
-INTERP Goal True.
-INTERP {
-INTERP exact I.
-INTERP }
-REWIND 1
+ADD { Goal True. }
+ADD { \{ }
+ADD here { exact I. }
+ADD { \} }
+EDIT_AT here
 # <replay>
-INTERP }
+ADD { \} }
 # </replay>
-INTERP Qed.
+ADD { Qed. }
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index f75e6fe9f..165b4130d 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -15,7 +15,7 @@ type coqtop = {
   xml_parser : Xml_parser.t;
 }
 
-let logger level content = ()
+let logger level content = prerr_endline content
 
 let base_eval_call ?(print=true) call coqtop =
   if print then prerr_endline (Serialize.pr_call call);
@@ -27,7 +27,7 @@ let base_eval_call ?(print=true) call coqtop =
       let message = Serialize.to_message xml in
       let level = message.Interface.message_level in
       let content = message.Interface.message_content in
-      let () = logger level content in
+      logger level content;
       loop ()
     else if Serialize.is_feedback xml then
       loop ()
@@ -39,63 +39,176 @@ let base_eval_call ?(print=true) call coqtop =
 
 let eval_call c q = ignore(base_eval_call c q)
 
+module Parser = struct
+
+  exception Err of string
+  exception More
+
+  type token =
+    | Tok of string * string
+    | Top of token list
+
+  type grammar =
+    | Alt of grammar list
+    | Seq of grammar list
+    | Opt of grammar
+    | Item of (string * (string -> token * int))
+
+  let eat_rex x = x, fun s ->
+    if Str.string_match (Str.regexp x) s 0 then begin
+      let m = Str.match_end () in
+      let w = String.sub s 0 m in
+      Tok(x,w), m
+    end else raise (Err ("Regexp "^x^" not found in: "^s))
+
+  let eat_balanced c =
+    let c' = match c with
+      | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in
+    let sc, sc' = String.make 1 c, String.make 1 c' in
+    let name = sc ^ "..." ^ sc' in
+    let unescape s =
+      Str.global_replace (Str.regexp ("\\\\"^sc)) sc
+        (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in
+    name, fun s ->
+    if s.[0] = c then
+      let rec find n m =
+        if String.length s <= m then raise More;
+        if s.[m] = c' then
+          if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1
+          else find (n-1) (m+1)
+        else if s.[m] = c then find (n+1) (m+1)
+        else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then
+          find n (m+2)
+        else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then
+          find n (m+2)
+        else find n (m+1)
+      in find ~-1 0
+    else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
+
+  let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+
+  let s = ref ""
+
+  let parse g =
+    let read_more () = s := !s ^ read_line () ^ "\n" in
+    let ensure_non_empty n = if n = String.length !s then read_more () in
+    let cut_after s n = String.sub s n (String.length s - n) in
+    let rec wrap f n =
+      try
+        ensure_non_empty n;
+        let _, n' = eat_blanks (cut_after !s n) in
+        ensure_non_empty n';
+        let t, m = f (cut_after !s (n+n')) in
+        let _, m' = eat_blanks (cut_after !s (n+n'+m)) in
+        t, n+n'+m+m'
+      with More -> read_more (); wrap f n in
+    let rec aux n g res : token list * int =
+      match g with
+      | Item (_,f) ->
+          let t, n = wrap f n in
+          t :: res, n
+      | Opt g ->
+          (try let res', n = aux n g [] in Top (List.rev res') :: res, n
+          with Err _ -> Top [] :: res, n)
+      | Alt gl ->
+          let rec fst = function
+            | [] -> raise (Err ("No more alternatives for: "^cut_after !s n))
+            | g :: gl ->
+               try aux n g res
+               with Err s -> fst gl in
+          fst gl
+      | Seq gl ->
+          let rec all (res,n) = function
+            | [] -> res, n
+            | g :: gl -> all (aux n g res) gl in
+          all (res,n) gl in
+    let res, n = aux 0 g [] in
+    s := cut_after !s n;
+    List.rev res
+
+  let clean s = Str.global_replace (Str.regexp "\n") "\\n" s
+
+  let rec print g =
+    match g with
+    | Item (s,_) -> Printf.sprintf " %s " (clean s)
+    | Opt g -> Printf.sprintf "[%s]" (print g)
+    | Alt gs -> Printf.sprintf "(%s)" (String.concat "\n|" (List.map print gs))
+    | Seq gs -> String.concat " " (List.map print gs)
+
+  let rec print_toklist = function
+    | [] -> ""
+    | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest
+    | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest
+    | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest
+
+end
+
 let ids = ref []
-let store_id = function
-  | Interface.Fail _ -> ()
-  | Interface.Good (id, _) -> ids := id :: !ids
-let rec erase_ids n =
-  if n = 0 then
-    match !ids with
-    | [] -> Stateid.initial
-    | x :: _ -> x
-  else match !ids with
-    | id :: rest -> ids := rest; erase_ids (n-1)
-    | [] -> exit 1
+let store_id s = function
+  | Interface.Fail (_,_,s) -> prerr_endline s; exit 1
+  | Interface.Good (id, _) -> ids := (s,id) :: !ids
+let rec erase_ids id = function
+  | Interface.Fail (_,_,s) -> prerr_endline s; exit 1
+  | Interface.Good (Util.Inl ()) ->
+      let rec aux () =
+        match !ids with
+        | [] -> ids := []
+        | (_, x) :: rest when Stateid.equal x id -> ()
+        | _ :: rest -> ids := rest; aux () in
+      aux ()
+  | Interface.Good (Util.Inr _) ->
+      prerr_endline "focusing not supported by fake ide";
+      exit 1
+let curid () = match !ids with (_,x) :: _ -> x | _ -> Stateid.initial
+let get_id id =
+  try List.assoc id !ids
+  with Not_found -> prerr_endline ("No state is named " ^ id); exit 1
+
 let eid = ref 0
 let edit () = incr eid; !eid
-let curid () = match !ids with x :: _ -> x | _ -> Stateid.initial
-
-let commands =
-  [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.query (s,Stateid.dummy)));
-    "INTERPRAW", (fun s -> eval_call (Serialize.query (s,Stateid.dummy)));
-    "INTERPSILENT", (fun s c ->
-      store_id (base_eval_call (Serialize.add ((s,edit()),(curid(),false))) c));
-    "INTERP", (fun s c ->
-      store_id (base_eval_call (Serialize.add ((s,edit()),(curid(),true))) c));
-    "REWIND", (fun s ->
-      let i = int_of_string s in
-      let id = erase_ids i in
-      eval_call (Serialize.edit_at id));
-    "GOALS", (fun _ -> eval_call (Serialize.goals ()));
-    "HINTS", (fun _ -> eval_call (Serialize.hints ()));
-    "GETOPTIONS", (fun _ -> eval_call (Serialize.get_options ()));
-    "STATUS", (fun _ -> eval_call (Serialize.status false));
-    "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s));
-    "MKCASES", (fun s -> eval_call (Serialize.mkcases s));
-    "#", (fun _ -> raise Comment);
-  ]
-
-let read_eval_print line =
-  let lline = String.length line in
-  let rec find_cmd = function
-    | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1
-    | (cmd,fn) :: cmds ->
-      let lcmd = String.length cmd in
-      if lline >= lcmd && String.sub line 0 lcmd = cmd then
-	let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> ""
-	in fn arg
-      else find_cmd cmds
-  in
-  find_cmd commands
+
+let eval_print l coq =
+  let open Parser in
+(*   prerr_endline ("Interpreting: " ^ print_toklist l); *)
+  match l with
+  | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] ->
+      store_id ""
+        (base_eval_call (Serialize.add ((phrase,edit()),(curid(),true))) coq)
+  | [ Tok(_,"ADD"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
+      store_id id
+        (base_eval_call (Serialize.add ((phrase,edit()),(curid(),true))) coq)
+  | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
+      erase_ids (get_id id)
+        (base_eval_call (Serialize.edit_at (get_id id)) coq)
+  | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
+      eval_call (Serialize.query (phrase,curid())) coq
+  | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
+      eval_call (Serialize.query (phrase,get_id id)) coq
+  | Tok("#[^\n]*",_) :: _  -> ()
+  | _ ->
+     prerr_endline "syntax error";
+     exit 1
+
+let grammar =
+  let open Parser in
+  let id = "[a-zA-Z_][a-zA-Z0-9_]*" in
+  let eat_phrase = eat_balanced '{' in
+  Alt
+    [ Seq [Item (eat_rex "ADD"); Opt (Item (eat_rex id)); Item eat_phrase]
+    ; Seq [Item (eat_rex "EDIT_AT"); Item (eat_rex id)]
+    ; Seq [Item (eat_rex "QUERY"); Opt (Item (eat_rex id)); Item eat_phrase]
+    ; Seq [Item (eat_rex "#[^\n]*")]
+    ]
+
+let read_command () = Parser.parse grammar
 
 let usage () =
   Printf.printf
     "A fake coqide process talking to a coqtop -ideslave.\n\
      Usage: %s [<coqtop>]\n\
-     Input syntax is one API call per line, the keyword coming first,\n\
-     with the rest of the line as string argument (e.g. INTERP Check plus.)\n\
-     Supported API keywords are:\n" (Filename.basename Sys.argv.(0));
-  List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands;
+     Input syntax is the following:\n%s\n"
+     (Filename.basename Sys.argv.(0))
+     (Parser.print grammar);
   exit 1
 
 let main =
@@ -118,17 +231,17 @@ let main =
     }
   in
   (match base_eval_call ~print:false (Serialize.init ()) coqtop with
-  | Interface.Good id -> ids := [id]
+  | Interface.Good id -> ids := ["initial",id]
   | Interface.Fail _ -> assert false);
   while true do
-    let l = try read_line () with End_of_file -> 
+    let l = try read_command () with End_of_file -> 
       match base_eval_call ~print:false (Serialize.status true) coqtop with
       | Interface.Good _ -> exit 0
       | Interface.Fail _ -> exit 1
     in
-    try read_eval_print l coqtop
+    try eval_print l coqtop
     with
       | Comment -> ()
       | e ->
-	prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1
+	prerr_endline ("Uncaught exception " ^ Printexc.to_string e); exit 1
   done