Coqide ported to STM

Main changes for STM:
1) protocol changed to carry edit/state ids
2) colouring reflects the actual status of every span (evaluated or not)
3) button to force the evaluation of the whole buffer
4) cmd_stack and backtracking completely changed to use state numbers
   instead of counting sentences
5) feedback messages are completely asynchronous, and the whole protocol
   could be made so with a minor effort, but there is little point in it
   right now.  Left as a future improvement.  Missing bit: add
   sentence-id to responses of interp command.

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

7 files changed, 149 insertions, 70 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d764894fa..f47901ad7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,6 +45,8 @@ let boot = ref false
 
 let batch_mode = ref false
 
+let ide_slave_mode = ref false
+
 let debug = ref false
 
 let print_emacs = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 388b33c12..c4ad3f333 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -12,6 +12,8 @@ val boot : bool ref
 
 val batch_mode : bool ref
 
+val ide_slave_mode : bool ref
+
 val debug : bool ref
 
 val print_emacs : bool ref
diff --git a/lib/interface.mli b/lib/interface.mli
index e1419da9b..274dbbb77 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -35,8 +35,6 @@ type status = {
   (** Current proof name. [None] if no focussed proof is in progress *)
   status_allproofs : string list;
   (** List of all pending proofs. Order is not significant *)
-  status_statenum : int;
-  (** A unique id describing the state of coqtop *)
   status_proofnum : int;
   (** An id describing the state of the current proof. *)
 }
@@ -119,14 +117,17 @@ type message = {
 
 (** Coq "semantic" infos obtained during parsing/execution *)
 type edit_id = int
+type state_id = Stateid.state_id
+type edit_or_state_id = Edit of edit_id | State of state_id
 
 type feedback_content =
   | AddedAxiom
   | Processed
   | GlobRef of Loc.t * string * string * string * string
+  | ErrorMsg of Loc.t * string
 
 type feedback = {
-  edit_id : edit_id;
+  id : edit_or_state_id;
   content : feedback_content;
 }
 
@@ -134,9 +135,11 @@ type feedback = {
 
 type location = (int * int) option (* start and end of the error *)
 
+(* The fail case carries the current state_id of the prover, the GUI
+   should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (location * string)
+  | Fail of (state_id * location * string)
 
 (* Request/Reply message protocol between Coq and CoqIde *)
 
@@ -146,18 +149,15 @@ type 'a value =
     of display options that coqide performs all the time.
     The returned string contains the messages produced
     but not the updated goals (they are
-    to be fetch by a separated [current_goals]). *)
+    to be fetch by a separated [current_goals]).
+    If edit_id=0 then the command is not part of the proof script,
+    and the resulting state_id is going to be dummy *)
 type interp_sty = edit_id * raw * verbose * string
-type interp_rty = string
+type interp_rty = state_id * string
 
-(** Backtracking by at least a certain number of phrases.
-    No finished proofs will be re-opened. Instead,
-    we continue backtracking until before these proofs,
-    and answer the amount of extra backtracking performed.
-    Backtracking by more than the number of phrases already
-    interpreted successfully (and not yet undone) will fail. *)
-type rewind_sty = int
-type rewind_rty = int
+(** Backtracking to a particular state *)
+type backto_sty = state_id
+type backto_rty = unit
 
 (** Fetching the list of current goals. Return [None] if no proof is in
     progress, [Some gl] otherwise. *)
@@ -174,8 +174,10 @@ type evars_rty = evar list option
 type hints_sty = unit
 type hints_rty = (hint list * hint) option
 
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-type status_sty = unit
+(** The status, for instance "Ready in SomeSection, proving Foo", the
+    input boolean (if true) forces the evaluation of all unevaluated
+    statements *)
+type status_sty = bool
 type status_rty = status
 
 (** Search for objects satisfying the given search flags. *)
@@ -206,15 +208,19 @@ type mkcases_rty = string list list
 type quit_sty = unit
 type quit_rty = unit
 
+(* Initialize, and return the initial state id *)
+type init_sty = unit
+type init_rty = state_id
+
 type about_sty = unit
 type about_rty = coq_info
 
-type handle_exn_rty = location * string
 type handle_exn_sty = exn
+type handle_exn_rty = state_id * location * string
 
 type handler = {
   interp      : interp_sty      -> interp_rty;
-  rewind      : rewind_sty      -> rewind_rty;
+  backto      : backto_sty      -> backto_rty;
   goals       : goals_sty       -> goals_rty;
   evars       : evars_sty       -> evars_rty;
   hints       : hints_sty       -> hints_rty;
@@ -224,8 +230,9 @@ type handler = {
   set_options : set_options_sty -> set_options_rty;
   inloadpath  : inloadpath_sty  -> inloadpath_rty;
   mkcases     : mkcases_sty     -> mkcases_rty;
-  quit        : quit_sty        -> quit_rty;
   about       : about_sty       -> about_rty;
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
+  init        : init_sty        -> init_rty;
+  quit        : quit_sty        -> quit_rty;
 }
 
diff --git a/lib/pp.ml b/lib/pp.ml
index c3cef6cda..331408b6d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -375,12 +375,15 @@ let set_logger l = logger := l
 (** Feedback *)
 
 let feeder = ref ignore
-let feedback_id = ref 0
+let feedback_id = ref (Interface.Edit 0)
 let set_id_for_feedback i = feedback_id := i
-let feedback what =
+let feedback ?state_id what =
   !feeder {
-     Interface.edit_id = !feedback_id;
-     Interface.content = what
+     Interface.content = what;
+     Interface.id =
+       match state_id with
+       | Some id -> Interface.State id
+       | None -> !feedback_id;
   }
 let set_feeder f = feeder := f
 
diff --git a/lib/pp.mli b/lib/pp.mli
index ccc6651ae..811dd4658 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -117,9 +117,10 @@ val set_logger : logger -> unit
  * during interpretation are attached to the exec_id (still unimplemented,
  * since the two phases are performed sequentially) *)
 
-val feedback : Interface.feedback_content -> unit
+val feedback :
+  ?state_id:Interface.state_id -> Interface.feedback_content -> unit
 
-val set_id_for_feedback : Interface.edit_id -> unit
+val set_id_for_feedback : Interface.edit_or_state_id -> unit
 val set_feeder : (Interface.feedback -> unit) -> unit
 
 (** {6 Utilities} *)
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 9fbd5683d..6636c24f0 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20120710"
+let protocol_version = "20130516"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -21,7 +21,7 @@ open Xml_datatype
 
 type 'a call =
   | Interp     of interp_sty
-  | Rewind     of rewind_sty
+  | Backto     of backto_sty
   | Goal       of goals_sty
   | Evars      of evars_sty
   | Hints      of hints_sty
@@ -33,13 +33,14 @@ type 'a call =
   | MkCases    of mkcases_sty
   | Quit       of quit_sty
   | About      of about_sty
+  | Init       of init_sty
 
 type unknown
 
 (** The actual calls *)
 
 let interp x      : interp_rty call      = Interp x
-let rewind x      : rewind_rty call      = Rewind x
+let backto x      : backto_rty call      = Backto x
 let goals x       : goals_rty call       = Goal x
 let evars x       : evars_rty call       = Evars x
 let hints x       : hints_rty call       = Hints x
@@ -50,6 +51,7 @@ let inloadpath x  : inloadpath_rty call  = InLoadPath x
 let mkcases x     : mkcases_rty call     = MkCases x
 let search x      : search_rty call      = Search x
 let quit x        : quit_rty call        = Quit x
+let init x        : init_rty call        = Init x
 
 (** * Coq answers to CoqIde *)
 
@@ -58,7 +60,7 @@ let abstract_eval_call handler (c : 'a call) =
   try
     match c with
       | Interp x     -> mkGood (handler.interp x)
-      | Rewind x     -> mkGood (handler.rewind x)
+      | Backto x     -> mkGood (handler.backto x)
       | Goal x       -> mkGood (handler.goals x)
       | Evars x      -> mkGood (handler.evars x)
       | Hints x      -> mkGood (handler.hints x)
@@ -70,6 +72,7 @@ let abstract_eval_call handler (c : 'a call) =
       | MkCases x    -> mkGood (handler.mkcases x)
       | Quit x       -> mkGood (handler.quit x)
       | About x      -> mkGood (handler.about x)
+      | Init x       -> mkGood (handler.init x)
   with any ->
     Fail (handler.handle_exn any)
 
@@ -83,36 +86,47 @@ module ReifType : sig
   val string_t       : string val_t
   val int_t          : int val_t
   val bool_t         : bool val_t
+  
+  val option_t       : 'a val_t -> 'a option val_t
+  val list_t         : 'a val_t -> 'a list val_t
+  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
+  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t
+
   val goals_t        : goals val_t
   val evar_t         : evar val_t
   val state_t        : status val_t
-  val coq_info_t     : coq_info val_t
   val option_state_t : option_state val_t
-  val option_t       : 'a val_t -> 'a option val_t
-  val list_t         : 'a val_t -> 'a list val_t
+  val coq_info_t     : coq_info val_t
   val coq_object_t   : 'a val_t -> 'a coq_object val_t
-  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
-  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t
+  val state_id_t     : state_id val_t
 
   type value_type = private
-    | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+    | Unit | String | Int | Bool
+
     | Option of value_type
     | List of value_type
-    | Coq_object of value_type
     | Pair of value_type * value_type
     | Union of value_type * value_type
+    
+    | Goals | Evar | State | Option_state | Coq_info
+    | Coq_object of value_type
+    | State_id
 
   val check : 'a val_t -> value_type
 
 end = struct
 
   type value_type =
-    | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+    | Unit | String | Int | Bool
+
     | Option of value_type
     | List of value_type
-    | Coq_object of value_type
     | Pair of value_type * value_type
     | Union of value_type * value_type
+    
+    | Goals | Evar | State | Option_state | Coq_info
+    | Coq_object of value_type
+    | State_id
 
   type 'a val_t = value_type
   let check x = x
@@ -121,16 +135,19 @@ end = struct
   let string_t       = String
   let int_t          = Int
   let bool_t         = Bool
+
+  let option_t x     = Option x
+  let list_t x       = List x
+  let pair_t x y     = Pair (x, y)
+  let union_t x y    = Union (x, y)
+
   let goals_t        = Goals
   let evar_t         = Evar
   let state_t        = State
-  let coq_info_t     = Coq_info
   let option_state_t = Option_state
-  let option_t x     = Option x
-  let list_t x       = List x
+  let coq_info_t     = Coq_info
   let coq_object_t x = Coq_object x
-  let pair_t x y     = Pair (x, y)
-  let union_t x y    = Union (x, y)
+  let state_id_t     = State_id
 
 end
 
@@ -143,9 +160,10 @@ let expected_answer_type call : value_type =
   let hints = pair_t (list_t hint) hint in
   let options = pair_t (list_t string_t) option_state_t in
   let objs = coq_object_t string_t in
+  let interp_t = pair_t state_id_t string_t in
   match call with
-  | Interp _     -> check (string_t                     : interp_rty      val_t)
-  | Rewind _     -> check (int_t                        : rewind_rty      val_t)
+  | Interp _     -> check (interp_t                     : interp_rty      val_t)
+  | Backto _     -> check (unit_t                       : backto_rty      val_t)
   | Goal _       -> check (option_t goals_t             : goals_rty       val_t)
   | Evars _      -> check (option_t (list_t evar_t)     : evars_rty       val_t)
   | Hints  _     -> check (option_t hints               : hints_rty       val_t)
@@ -157,6 +175,7 @@ let expected_answer_type call : value_type =
   | MkCases _    -> check (list_t (list_t string_t)     : mkcases_rty     val_t)
   | Quit _       -> check (unit_t                       : quit_rty        val_t)
   | About _      -> check (coq_info_t                   : about_rty       val_t)
+  | Init _       -> check (state_id_t                   : init_rty        val_t)
 
 (** * XML data marshalling *)
 
@@ -327,15 +346,38 @@ let to_coq_object f = function
   }
 | _ -> raise Marshal_error
 
+let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
+let to_edit_id = function
+  | Element ("edit_id",["val",i],[]) ->
+      let id = int_of_string i in
+      assert (id <= 0 );
+      id
+  | _ -> raise Marshal_error
+
+let of_state_id id =
+  try Stateid.of_state_id id with Invalid_argument _ -> raise Marshal_error
+let to_state_id xml =
+  try Stateid.to_state_id xml with Invalid_argument _ -> raise Marshal_error
+
+let of_edit_or_state_id = function
+  | Interface.Edit id -> ["object","edit"], of_edit_id id
+  | Interface.State id -> ["object","state"], of_state_id id
+let to_edit_or_state_id attrs xml =
+  try
+    let obj = List.assoc "object" attrs in
+    if obj = "edit"then Interface.Edit (to_edit_id xml)
+    else if obj = "state" then Interface.State (to_state_id xml)
+    else raise Marshal_error
+  with Not_found -> raise Marshal_error
+
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
-| Fail (loc, msg) ->
+| Fail (id,loc, msg) ->
   let loc = match loc with
   | None -> []
-  | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)]
-  in
-  Element ("value", ["val", "fail"] @ loc, [PCData msg])
-
+  | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
+  let id = of_state_id id in
+  Element ("value", ["val", "fail"] @ loc, [id;PCData msg])
 let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
@@ -348,8 +390,9 @@ let to_value f = function
         Some (loc_s, loc_e)
       with Not_found | Failure _ -> None
     in
-    let msg = raw_string l in
-    Fail (loc, msg)
+    let id = to_state_id (List.hd l) in
+    let msg = raw_string (List.tl l) in
+    Fail (id, loc, msg)
   else raise Marshal_error
 | _ -> raise Marshal_error
 
@@ -358,16 +401,16 @@ let of_call = function
   let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
   Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags,
   [PCData cmd])
-| Rewind n ->
-  Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
+| Backto id ->
+  Element ("call", ["val", "backto"], [of_state_id id])
 | Goal () ->
   Element ("call", ["val", "goal"], [])
 | Evars () ->
   Element ("call", ["val", "evars"], [])
 | Hints () ->
   Element ("call", ["val", "hints"], [])
-| Status () ->
-  Element ("call", ["val", "status"], [])
+| Status b ->
+  Element ("call", ["val", "status";"force",string_of_bool b], [])
 | Search flags ->
   let args = List.map (of_pair of_search_constraint of_bool) flags in
   Element ("call", ["val", "search"], args)
@@ -384,6 +427,8 @@ let of_call = function
   Element ("call", ["val", "quit"], [])
 | About () ->
   Element ("call", ["val", "about"], [])
+| Init () ->
+  Element ("call", ["val", "init"], [])
 
 let to_call = function
 | Element ("call", attrs, l) ->
@@ -394,12 +439,15 @@ let to_call = function
     let raw = List.mem_assoc "raw" attrs in
     let vrb = List.mem_assoc "verbose" attrs in
     Interp (int_of_string id, raw, vrb, raw_string l)
-  | "rewind" ->
-    let steps = int_of_string (massoc "steps" attrs) in
-    Rewind steps
+  | "backto" ->
+      (match l with
+      | [id] -> Backto(to_state_id id)
+      | _ -> raise Marshal_error)
   | "goal" -> Goal ()
   | "evars" -> Evars ()
-  | "status" -> Status ()
+  | "status" ->
+      let force = List.assoc "force" attrs in
+      Status (bool_of_string force)
   | "search" ->
     let args = List.map (to_pair to_search_constraint to_bool) l in
     Search args
@@ -412,6 +460,7 @@ let to_call = function
   | "hints" -> Hints ()
   | "quit" -> Quit ()
   | "about" -> About ()
+  | "init" -> Init ()
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -424,18 +473,16 @@ let of_status s =
       of_sl s.status_path;
       of_so s.status_proofname;
       of_sl s.status_allproofs;
-      of_int s.status_statenum;
       of_int s.status_proofnum;
     ]
   )
 
 let to_status = function
-| Element ("status", [], [path; name; prfs; snum; pnum]) ->
+| Element ("status", [], [path; name; prfs; pnum]) ->
   {
     status_path = to_list to_string path;
     status_proofname = to_option to_string name;
     status_allproofs = to_list to_string prfs;
-    status_statenum = to_int snum;
     status_proofnum = to_int pnum;
   }
 | _ -> raise Marshal_error
@@ -545,6 +592,10 @@ let to_feedback_content xml = do_match xml "feedback_content"
             GlobRef(to_loc loc, to_string filepath, to_string modpath,
                     to_string ident, to_string ty)
        | _ -> raise Marshal_error)
+  | "errormsg" ->
+       (match args with
+       | [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
+       | _ -> raise Marshal_error)
   | _ -> raise Marshal_error)
 
 let of_feedback_content = function
@@ -558,14 +609,19 @@ let of_feedback_content = function
       of_string ident;
       of_string ty
     ]
+| ErrorMsg(loc, s) ->
+    constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in
-  Element ("feedback", ["id",string_of_int msg.edit_id], [content])
+  let obj, id = of_edit_or_state_id msg.id in
+  Element ("feedback", obj, [id;content])
 
 let to_feedback xml = match xml with
-| Element ("feedback", ["id",id], [content]) ->
-  { edit_id = int_of_string id;
+| Element ("feedback", ["object","edit"], [id;content]) ->
+  { id = Interface.Edit(to_edit_id id); content = to_feedback_content content }
+| Element ("feedback", ["object","state"], [id;content]) ->
+  { id = Interface.State(to_state_id id);
     content = to_feedback_content content }
 | _ -> raise Marshal_error
 
@@ -596,6 +652,7 @@ let of_answer (q : 'a call) (r : 'a value) : xml =
     | Coq_object t  -> Obj.magic (of_coq_object (convert t))
     | Pair (t1,t2)  -> Obj.magic (of_pair (convert t1) (convert t2))
     | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
+    | State_id      -> Obj.magic of_state_id
   in
   of_value (convert (expected_answer_type q)) r
 
@@ -615,6 +672,7 @@ let to_answer xml (c : 'a call) : 'a value =
     | Coq_object t  -> Obj.magic (to_coq_object (convert t))
     | Pair (t1,t2)  -> Obj.magic (to_pair (convert t1) (convert t2))
     | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
+    | State_id      -> Obj.magic to_state_id
   in
   to_value (convert (expected_answer_type c)) xml
 
@@ -669,11 +727,11 @@ let pr_call = function
     let raw = if r then "RAW" else "" in
     let verb = if b then "" else "SILENT" in
     "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
-  | Rewind i -> "REWIND "^(string_of_int i)
+  | Backto i -> "BACKTO "^(Stateid.string_of_state_id i)
   | Goal _ -> "GOALS"
   | Evars _ -> "EVARS"
   | Hints _ -> "HINTS"
-  | Status _ -> "STATUS"
+  | Status b -> "STATUS " ^ string_of_bool b
   | Search _ -> "SEARCH"
   | GetOptions _ -> "GETOPTIONS"
   | SetOptions l -> "SETOPTIONS" ^ " [" ^
@@ -683,9 +741,13 @@ let pr_call = function
   | MkCases s -> "MKCASES "^s
   | Quit _ -> "QUIT"
   | About _ -> "ABOUT"
+  | Init _ -> "INIT"
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (_,str) -> "FAIL ["^str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.string_of_state_id id^" ["^str^"]"
+  | Fail (id,Some(i,j),str) ->
+      "FAIL "^Stateid.string_of_state_id id^
+        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value =
   let rec pr = function
@@ -703,5 +765,6 @@ let pr_full_value call value =
   | Coq_object t  -> Obj.magic pr_coq_object
   | Pair (t1,t2)  -> Obj.magic (pr_pair (pr t1) (pr t2))
   | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2))
+  | State_id      -> Obj.magic pr_int
   in
   pr_value_gen (pr (expected_answer_type call)) value
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 48c699a2f..00e95be2e 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -16,7 +16,7 @@ type 'a call
 type unknown
 
 val interp      : interp_sty      -> interp_rty call
-val rewind      : rewind_sty      -> rewind_rty call
+val backto      : backto_sty      -> backto_rty call
 val goals       : goals_sty       -> goals_rty call
 val hints       : hints_sty       -> hints_rty call
 val status      : status_sty      -> status_rty call
@@ -27,6 +27,7 @@ val search      : search_sty      -> search_rty call
 val get_options : get_options_sty -> get_options_rty call
 val set_options : set_options_sty -> set_options_rty call
 val quit        : quit_sty        -> quit_rty call
+val init        : init_sty        -> init_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value