fake_ide: ported to Document + 2 tests for editing a proof (locally)

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

5 files changed, 201 insertions, 83 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f47b0aa0c..cc39e8ac2 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -434,7 +434,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(BIN)fake_ide "$(BIN)coqtop -boot" < $< 2>&1; \
+	  $(BIN)fake_ide $< "$(BIN)coqtop -boot -coq-slaves on -coq-slaves-opts min-proof-length-to-delegate=0" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
index 770350fbd..7a1dc81e0 100644
--- a/test-suite/ide/undo007.fake
+++ b/test-suite/ide/undo007.fake
@@ -11,11 +11,10 @@ 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 { Stm PrintDag. }
+# QUERY { Stm Finish. }
 QUERY { Print d. }
 QUERY { Check e. }
diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake
new file mode 100644
index 000000000..2adde908d
--- /dev/null
+++ b/test-suite/ide/undo020.fake
@@ -0,0 +1,27 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# focusing a broken proof and fixing it
+ 
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { idtac. }
+ADD { exact Ix. }
+ADD { Qed. }
+# second proof
+ADD { Lemma b : False. }
+ADD { Proof using. }
+ADD { admit. }
+ADD last { Qed. }
+# We join and expect some proof to fail
+WAIT
+# Going back to the error
+EDIT_AT here
+# Fixing the proof
+ADD { exact I. }
+ADD { Qed. }
+# we are back at the end
+ASSERT TIP last
+QUERY { Check a. }
+QUERY { Check b. }
diff --git a/test-suite/ide/undo021.fake b/test-suite/ide/undo021.fake
new file mode 100644
index 000000000..0d83ad25a
--- /dev/null
+++ b/test-suite/ide/undo021.fake
@@ -0,0 +1,29 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs
+ 
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { idtac. }
+ADD { exact Ix. }
+ADD { Qed. }
+# second proof
+ADD { Lemma b : True. }
+ADD here2 { Proof using. }
+ADD { exact Ix. }
+ADD { Qed. }
+# We wait all slaves and expect both proofs to fail
+WAIT
+# Going back to the error
+EDIT_AT here2
+# this is not implemented yet, all after here is erased 
+EDIT_AT here
+# Fixing the proof
+ADD { exact I. }
+ADD last { Qed. }
+ASSERT TIP last
+# we are back at the end
+QUERY { Check a. }
+QUERY { Fail Check b. }
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 165b4130d..c66db8bfe 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -8,7 +8,9 @@
 
 (** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
 
-exception Comment
+let error s =
+  prerr_endline ("fake_id: error: "^s);
+  exit 1
 
 type coqtop = {
   xml_printer : Xml_printer.t;
@@ -17,7 +19,7 @@ type coqtop = {
 
 let logger level content = prerr_endline content
 
-let base_eval_call ?(print=true) call coqtop =
+let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Serialize.pr_call call);
   let xml_query = Serialize.of_call call in
   Xml_printer.print coqtop.xml_printer xml_query;
@@ -35,11 +37,14 @@ let base_eval_call ?(print=true) call coqtop =
   in
   let res = loop () in
   if print then prerr_endline (Serialize.pr_full_value call res);
-  match res with Interface.Fail _ -> exit 1 | x -> x
+  match res with
+  | Interface.Fail (_,_,s) when fail -> error s
+  | Interface.Fail (_,_,s) as x -> prerr_endline s; x
+  | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
 
-module Parser = struct
+module Parser = struct (* {{{ *)
 
   exception Err of string
   exception More
@@ -89,8 +94,8 @@ module Parser = struct
 
   let s = ref ""
 
-  let parse g =
-    let read_more () = s := !s ^ read_line () ^ "\n" in
+  let parse g ic =
+    let read_more () = s := !s ^ input_line ic ^ "\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 =
@@ -130,9 +135,9 @@ module Parser = struct
 
   let rec print g =
     match g with
-    | Item (s,_) -> Printf.sprintf " %s " (clean s)
+    | 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))
+    | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
     | Seq gs -> String.concat " " (List.map print gs)
 
   let rec print_toklist = function
@@ -141,107 +146,165 @@ module Parser = struct
     | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest
     | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest
 
+end (* }}} *)
+
+type sentence = {
+  name : string;
+  text : string;
+  edit_id : int;
+}
+
+let doc : sentence Document.document = Document.create ()
+
+let tip_id () =
+  try Document.tip doc
+  with
+  | Document.Empty -> Stateid.initial
+  | Invalid_argument _ -> error "add_sentence on top of non assigned tip"
+
+let add_sentence =
+  let edit_id = ref 0 in
+  fun ?(name="") text ->
+    let tip_id = tip_id () in
+    decr edit_id;
+    Document.push doc { name; text; edit_id = !edit_id };
+    !edit_id, tip_id
+
+let print_document () =
+  let ellipsize s =
+          Str.global_replace (Str.regexp "^[\n ]*") ""
+      (if String.length s > 20 then String.sub s 0 17 ^ "..."
+       else s) in
+  prerr_endline (Pp.string_of_ppcmds
+    (Document.print doc
+      (fun b state_id { name; text } ->
+        Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
+          (if b then "*" else " ")
+          name
+          (Stateid.to_string (Option.default Stateid.dummy state_id))
+          (ellipsize text)))))
+
+(* This module is the logic a GUI has to implement *)
+module GUILogic = struct
+
+  let after_add = function
+    | Interface.Fail (_,_,s) -> error s
+    | Interface.Good (id, (Util.Inl (), _)) ->
+        Document.assign_tip_id doc id
+    | Interface.Good (id, (Util.Inr tip, _)) ->
+        Document.assign_tip_id doc id;
+        Document.unfocus doc;
+        ignore(Document.cut_at doc tip);
+        print_document ()
+  
+  let at id id' _ = Stateid.equal id' id
+  
+  let after_edit_at (id,need_unfocus) = function
+    | Interface.Fail (_,_,s) -> error s
+    | Interface.Good (Util.Inl ()) ->
+        if need_unfocus then Document.unfocus doc;
+        ignore(Document.cut_at doc id);
+        print_document ()
+    | Interface.Good (Util.Inr (stop_id,(start_id,tip))) ->
+        if need_unfocus then Document.unfocus doc;
+        ignore(Document.cut_at doc tip);
+        Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
+        ignore(Document.cut_at doc id);
+        print_document ()
+  
+  let get_id id =
+    try Document.find_id doc (fun _ { name } -> name = id)
+    with Not_found -> error ("No state is named " ^ id)
+
 end
 
-let ids = ref []
-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
+open GUILogic
 
 let eval_print l coq =
   let open Parser in
-(*   prerr_endline ("Interpreting: " ^ print_toklist l); *)
+  let open Serialize 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)
+      let eid, tip = add_sentence phrase in
+      after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+  | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
+      let eid, tip = add_sentence ~name phrase in
+      after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
   | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
-      erase_ids (get_id id)
-        (base_eval_call (Serialize.edit_at (get_id id)) coq)
+      let to_id, need_unfocus = get_id id in
+      after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
   | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
-      eval_call (Serialize.query (phrase,curid())) coq
+      eval_call (query (phrase,tip_id())) coq
   | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
-      eval_call (Serialize.query (phrase,get_id id)) coq
+      let to_id, _ = get_id id in
+      eval_call (query (phrase, to_id)) coq
+  | [ Tok(_,"WAIT") ] ->
+      let phrase = "Stm Wait." in
+      eval_call (query (phrase,tip_id())) coq
+  | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
+      let to_id, _ = get_id id in
+      if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
+      else prerr_endline "Good tip"
   | Tok("#[^\n]*",_) :: _  -> ()
-  | _ ->
-     prerr_endline "syntax error";
-     exit 1
+  | _ -> error "syntax error"
 
 let grammar =
   let open Parser in
-  let id = "[a-zA-Z_][a-zA-Z0-9_]*" in
+  let eat_id = eat_rex "[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]*")]
+    [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
+    ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "WAIT")]
+    ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
+    ; Item (eat_rex "#[^\n]*")
     ]
 
-let read_command () = Parser.parse grammar
+let read_command inc = Parser.parse grammar inc
 
 let usage () =
-  Printf.printf
+  error (Printf.sprintf
     "A fake coqide process talking to a coqtop -ideslave.\n\
-     Usage: %s [<coqtop>]\n\
+     Usage: %s (file|-) [<coqtop>]\n\
      Input syntax is the following:\n%s\n"
      (Filename.basename Sys.argv.(0))
-     (Parser.print grammar);
-  exit 1
+     (Parser.print grammar))
 
 let main =
   Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let coqtop_name = match Array.length Sys.argv with
-    | 1 -> "coqtop"
-    | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1)
-    | _ -> usage ()
-  in
-  let coqtop =
+  let coqtop_name, input_file = match Sys.argv with
+    | [| _; f |] -> "coqtop", f
+    | [| _; f; ct |] -> ct, f
+    | _ -> usage () in
+  let inc = if input_file = "-" then stdin else open_in input_file in
+  let coq =
     let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
     let ip = Xml_parser.make (Xml_parser.SChannel cin) in
     let op = Xml_printer.make (Xml_printer.TChannel cout) in
-    let () = Xml_parser.check_eof ip false in
-    {
-      xml_printer = op;
-      xml_parser = ip;
-    }
-  in
-  (match base_eval_call ~print:false (Serialize.init ()) coqtop with
-  | Interface.Good id -> ids := ["initial",id]
-  | Interface.Fail _ -> assert false);
+    Xml_parser.check_eof ip false;
+    { xml_printer = op; xml_parser = ip } in
+  let init () =
+    match base_eval_call ~print:false (Serialize.init ()) coq with
+    | Interface.Good id ->
+        let dir = Filename.dirname input_file in
+        let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
+        let eid, tip = add_sentence ~name:"initial" phrase in
+        after_add (base_eval_call (Serialize.add ((phrase,eid),(tip,true))) coq)
+    | Interface.Fail _ -> error "init call failed" in
+  let finish () =
+    match base_eval_call (Serialize.status true) coq with
+    | Interface.Good _ -> exit 0
+    | Interface.Fail (_,_,s) -> error s in
+  (* The main loop *)
+  init ();
   while true do
-    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 eval_print l coqtop
-    with
-      | Comment -> ()
-      | e ->
-	prerr_endline ("Uncaught exception " ^ Printexc.to_string e); exit 1
+    let cmd = try read_command inc with End_of_file -> finish () in
+    try eval_print cmd coq
+    with e -> error ("Uncaught exception " ^ Printexc.to_string e)
   done
+
+(* vim:set foldmethod=marker: *)