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

25 files changed, 527 insertions, 349 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index beece5497..718eb718f 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -99,6 +99,7 @@
 	      <keyword>then</keyword>
 	      <keyword>else</keyword>
 	      <keyword>return</keyword>
+	      <keyword>using</keyword>
 	    </context>
 	    <context id="constr-sort" style-ref="constr-sort">
 	      <keyword>Prop</keyword>
diff --git a/ide/coq.ml b/ide/coq.ml
index 27566c6ca..b9b7c1d45 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -347,34 +347,29 @@ let open_process_pid prog args =
 exception TubeError
 exception AnswerWithoutRequest
 
-(* Check that a string is only composed by blank characters
-   from a position onwards *)
-let is_blank s pos =
-  try
-    for i = pos to String.length s - 1 do
-      if not (List.mem s.[i] [' ';'\n';'\t';'\r']) then raise Not_found
-    done;
-    true
-  with Not_found -> false
-
 let rec check_errors = function
 | [] -> ()
 | (`IN | `PRI) :: conds -> check_errors conds
 | e :: _ -> raise TubeError
 
-let handle_intermediate_message logger xml =
+let handle_intermediate_message handle xml =
   let message = Serialize.to_message xml in
   let level = message.Interface.message_level in
   let content = message.Interface.message_content in
+  let logger = match handle.waiting_for with
+    | None -> raise AnswerWithoutRequest
+    | Some (_, l) -> l in
   logger level content
 
 let handle_feedback feedback_processor xml =
-  let () = Minilib.log "Handling some feedback" in
   let feedback = Serialize.to_feedback xml in
   feedback_processor feedback
 
-let handle_final_answer handle ccb xml =
+let handle_final_answer handle xml =
   let () = Minilib.log "Handling coqtop answer" in
+  let ccb = match handle.waiting_for with
+    | None -> raise AnswerWithoutRequest
+    | Some (c, _) -> c in
   let () = handle.waiting_for <- None in
   with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer xml c) }
 
@@ -390,33 +385,22 @@ let unsafe_handle_input handle feedback_processor state conds =
   let () = if String.length s = 0 then raise TubeError in
   let s = state.fragment ^ s in
   let () = state.fragment <- s in
-  let ccb, logger = match handle.waiting_for with
-  | None -> raise AnswerWithoutRequest
-  | Some (c, l) -> c, l
-  in
   let lex = Lexing.from_string s in
   let p = Xml_parser.make (Xml_parser.SLexbuf lex) in
   let rec loop () =
     let xml = Xml_parser.parse p in
     let l_end = Lexing.lexeme_end lex in
-    if Serialize.is_message xml then
-      let remaining = String.sub s l_end (String.length s - l_end) in
-      let () = state.fragment <- remaining in
-      let () = state.lexerror <- None in
-      let () = handle_intermediate_message logger xml in
+    state.fragment <- String.sub s l_end (String.length s - l_end);
+    state.lexerror <- None;
+    if Serialize.is_message xml then begin
+      handle_intermediate_message handle xml;
       loop ()
-    else if Serialize.is_feedback xml then
-      let remaining = String.sub s l_end (String.length s - l_end) in
-      let () = state.fragment <- remaining in
-      let () = state.lexerror <- None in
-      let () = handle_feedback feedback_processor xml in
+    end else if Serialize.is_feedback xml then begin
+      handle_feedback feedback_processor xml;
       loop ()
-    else
-      (* We should have finished decoding s *)
-      let () = if not (is_blank s l_end) then raise AnswerWithoutRequest in
-      let () = state.fragment <- "" in
-      let () = state.lexerror <- None in
-      ignore (handle_final_answer handle ccb xml)
+    end else begin
+      ignore (handle_final_answer handle xml)
+    end
   in
   try loop ()
   with Xml_parser.Error _ as e ->
@@ -576,12 +560,13 @@ let eval_call ?(logger=default_logger) call handle k =
 
 let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s =
   eval_call ~logger (Serialize.interp (i,raw,verbose,s))
-let rewind i = eval_call (Serialize.rewind i)
+let backto i = eval_call (Serialize.backto i)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
-let status = eval_call (Serialize.status ())
-let hints = eval_call (Serialize.hints ())
+let status ?logger force = eval_call ?logger (Serialize.status force)
+let hints x = eval_call (Serialize.hints x)
 let search flags = eval_call (Serialize.search flags)
+let init x = eval_call (Serialize.init x)
 
 module PrintOpt =
 struct
@@ -645,8 +630,8 @@ struct
 
 end
 
-let goals h k =
-  PrintOpt.enforce h (fun () -> eval_call (Serialize.goals ()) h k)
+let goals ?logger x h k =
+  PrintOpt.enforce h (fun () -> eval_call ?logger (Serialize.goals x) h k)
 
-let evars h k =
-  PrintOpt.enforce h (fun () -> eval_call (Serialize.evars ()) h k)
+let evars x h k =
+  PrintOpt.enforce h (fun () -> eval_call (Serialize.evars x) h k)
diff --git a/ide/coq.mli b/ide/coq.mli
index ed78e96e2..330cc776f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -122,19 +122,21 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val interp :
-  ?logger:Ideutils.logger ->
+val interp : ?logger:Ideutils.logger ->
   ?raw:bool ->
   ?verbose:bool ->
-    int -> string -> string query
-val rewind : int -> int query
-val status : Interface.status query
-val goals : Interface.goals option query
-val evars : Interface.evar list option query
-val hints : (Interface.hint list * Interface.hint) option query
-val inloadpath : string -> bool query
-val mkcases : string -> string list list query
-val search : Interface.search_flags -> string Interface.coq_object list query
+    Interface.edit_id -> string           -> Interface.interp_rty query
+val backto     : Interface.backto_sty     -> Interface.backto_rty query
+val status     : ?logger:Ideutils.logger ->
+                 Interface.status_sty -> Interface.status_rty query
+val goals      : ?logger:Ideutils.logger ->
+                 Interface.goals_sty      -> Interface.goals_rty query
+val evars      : Interface.evars_sty      -> Interface.evars_rty query
+val hints      : Interface.hints_sty      -> Interface.hints_rty query
+val inloadpath : Interface.inloadpath_sty -> Interface.inloadpath_rty query
+val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
+val search     : Interface.search_sty     -> Interface.search_rty query
+val init       : Interface.init_sty       -> Interface.init_rty query
 
 (** A specialized version of [raw_interp] dedicated to set/unset options. *)
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 15ca34b2f..4105bd82a 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -8,8 +8,9 @@
 
 open Coq
 open Ideutils
+open Interface
 
-type flag = [ `COMMENT | `UNSAFE ]
+type flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ]
 
 module SentenceId : sig
 
@@ -17,12 +18,19 @@ module SentenceId : sig
     start : GText.mark;
     stop : GText.mark;
     mutable flags : flag list;
-    id : int;
+    edit_id : int;
+    mutable state_id : Stateid.state_id option;
   }
 
   val mk_sentence :
     start:GText.mark -> stop:GText.mark -> flag list -> sentence
+
+  val assign_state_id : sentence -> Stateid.state_id -> unit
   val set_flags : sentence -> flag list -> unit
+  val add_flag : sentence -> flag -> unit
+  val remove_flag : sentence -> flag -> unit
+  val same_sentence : sentence -> sentence -> bool
+  val hidden_edit_id : unit -> int
 
 end = struct
 
@@ -30,7 +38,8 @@ end = struct
     start : GText.mark;
     stop : GText.mark;
     mutable flags : flag list;
-    id : int;
+    edit_id : int;
+    mutable state_id : Stateid.state_id option;
   }
 
   let id = ref 0
@@ -38,10 +47,19 @@ end = struct
     start = start;
     stop = stop;
     flags = flags;
-    id = !id;
+    edit_id = !id;
+    state_id = None;
   }
+  let hidden_edit_id () = decr id; !id
 
+  let assign_state_id s id =
+    assert(s.state_id = None);
+    assert(id <> Stateid.dummy_state_id);
+    s.state_id <- Some id
   let set_flags s f = s.flags <- f
+  let add_flag s f = s.flags <- CList.add_set f s.flags
+  let remove_flag s f = s.flags <- CList.remove f s.flags
+  let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id
 
 end
 open SentenceId
@@ -62,6 +80,11 @@ object
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
+  method join_document : unit task
+
+  method handle_failure : handle_exn_rty -> unit task
+
+  method destroy : unit -> unit
 end
 
 class coqops
@@ -76,11 +99,20 @@ object(self)
   val proof = _pv
   val messages = _mv
 
-  val cmd_stack = Stack.create ()
+  val cmd_stack = Searchstack.create ()
+
+  val mutable initial_state = Stateid.initial_state_id
+
+  val feedbacks : feedback Queue.t = Queue.create ()
+  val feedback_timer = Ideutils.mktimer ()
 
   initializer
-    Coq.set_feedback_handler _ct self#process_feedback;
-    Wg_Tooltip.set_tooltip_callback (script :> GText.view)
+    Coq.set_feedback_handler _ct self#enqueue_feedback;
+    Wg_Tooltip.set_tooltip_callback (script :> GText.view);
+    feedback_timer.Ideutils.run ~ms:250 ~callback:self#process_feedback
+
+  method destroy () =
+    feedback_timer.Ideutils.kill ()
 
   method private get_start_of_input =
     buffer#get_iter_at_mark (`NAME "start_of_input")
@@ -90,16 +122,12 @@ object(self)
 
   method show_goals =
     Coq.PrintOpt.set_printing_width proof#width;
-    Coq.bind Coq.goals (function
-    | Interface.Fail (l, str) ->
-      messages#set ("Error in coqtop:\n"^str);
-      Coq.return ()
-    | Interface.Good goals ->
-      Coq.bind Coq.evars (function
-        | Interface.Fail (l, str)->
-          messages#set ("Error in coqtop:\n"^str);
-          Coq.return ()
-        | Interface.Good evs ->
+    Coq.bind (Coq.goals ~logger:messages#push ()) (function
+    | Fail x -> self#handle_failure x
+    | Good goals ->
+      Coq.bind (Coq.evars ()) (function
+        | Fail x -> self#handle_failure x
+        | Good evs ->
           proof#set_goals goals;
           proof#set_evars evs;
           proof#refresh ();
@@ -118,8 +146,8 @@ object(self)
     let query =
       Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
     let next = function
-    | Interface.Fail (_, err) -> display_error err; Coq.return ()
-    | Interface.Good msg ->
+    | Fail (_, _, err) -> display_error err; Coq.return () (* XXX*)
+    | Good (_, msg) ->
       messages#add msg; Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
@@ -161,16 +189,25 @@ object(self)
   method private mark_as_needed sentence =
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
-    let tag =
-      if List.mem `UNSAFE sentence.flags then Tags.Script.unjustified
-      else Tags.Script.processed in
-    buffer#apply_tag tag ~start ~stop
+    let to_process = Tags.Script.to_process in
+    let processed = Tags.Script.processed in
+    let unjustified = Tags.Script.unjustified in
+    let error_bg = Tags.Script.error_bg in
+    let all_tags = [ to_process; processed; unjustified ] in
+    let tags =
+      (if List.mem `PROCESSING sentence.flags then to_process else
+       if List.mem `ERROR sentence.flags then error_bg else
+       processed)
+      ::
+      (if [ `UNSAFE ] = sentence.flags then [unjustified] else [])
+    in
+    List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
+    List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
 
   method private attach_tooltip sentence loc text =
-    let pre_chars, post_chars = Loc.unloc loc in
-    let start_sentence = buffer#get_iter_at_mark sentence.start in
-    let stop_sentence = buffer#get_iter_at_mark sentence.stop in
-    let phrase = start_sentence#get_slice ~stop:stop_sentence in
+    let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
+    let pre_chars, post_chars =
+      if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in
     let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
     let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
     let start = start_sentence#forward_chars pre in
@@ -178,60 +215,106 @@ object(self)
     let markup = lazy text in
     Wg_Tooltip.apply_tooltip_tag buffer ~start ~stop ~markup
 
-  method private process_feedback msg =
-    let id = msg.Interface.edit_id in
-    if id = 0 || Stack.is_empty cmd_stack then () else
-    let sentence =
-      let last_sentence = Stack.top cmd_stack in
-      if last_sentence.id = id then Some last_sentence else None in
-    match msg.Interface.content, sentence with
-    | Interface.AddedAxiom, Some sentence ->
-        set_flags sentence (CList.add_set `UNSAFE sentence.flags);
-        self#mark_as_needed sentence
-    | Interface.Processed, Some sentence -> self#mark_as_needed sentence
-    | Interface.GlobRef(loc, filepath, modpath, ident, ty), Some sentence ->
-        self#attach_tooltip sentence loc
-          (Printf.sprintf "%s %s %s" filepath ident ty)
-    | _ ->
-        if sentence = None then
-          Minilib.log "Coqide/Coq is really asynchronous now!"
-          (* In this case we shoud look for (exec_)id into cmd_stack *)
-        else Minilib.log "Unsupported feedback message"
+  method private is_dummy_id id =
+    match id with
+    | Edit 0 -> true
+    | State id when id = Stateid.dummy_state_id -> true
+    | _ -> false
+
+  method private enqueue_feedback msg =
+    let id = msg.id in
+    if self#is_dummy_id id then () else Queue.add msg feedbacks
+    
+  method private process_feedback () =
+    let rec eat_feedback n =
+      if n = 0 then true else
+      let msg = Queue.pop feedbacks in
+      let id = msg.id in
+      let sentence =
+        let finder () s =
+          match s.state_id, id with
+          | Some id', State id when id = id' -> `Stop s
+          | _, Edit id when id = s.edit_id -> `Stop s
+          | _ -> `Cont () in
+        try Some (Searchstack.find finder () cmd_stack)
+        with Not_found -> None in
+      let log s sentence =
+        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.string_of_state_id
+          (Option.default Stateid.dummy_state_id sentence.state_id)) in
+      begin match msg.content, sentence with
+      | AddedAxiom, Some sentence ->
+          log "AddedAxiom" sentence;
+          remove_flag sentence `PROCESSING;
+          remove_flag sentence `ERROR;
+          add_flag sentence `UNSAFE;
+          self#mark_as_needed sentence
+      | Processed, Some sentence ->
+          log "Processed" sentence;
+          remove_flag sentence `PROCESSING;
+          remove_flag sentence `ERROR;
+          self#mark_as_needed sentence
+      | GlobRef(loc, filepath, modpath, ident, ty), Some sentence ->
+          log "GlobRef" sentence;
+          self#attach_tooltip sentence loc
+            (Printf.sprintf "%s %s %s" filepath ident ty)
+      | ErrorMsg(loc, msg), Some sentence ->
+          log "ErrorMsg" sentence;
+          remove_flag sentence `PROCESSING;
+          add_flag sentence `ERROR;
+          self#mark_as_needed sentence;
+          self#attach_tooltip sentence loc msg;
+          if not (Loc.is_ghost loc) then
+            self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
+      | _ ->
+          if sentence <> None then Minilib.log "Unsupported feedback message"
+          else if Searchstack.is_empty cmd_stack then ()
+          else
+            match id, (Searchstack.top cmd_stack).state_id with
+            | Edit _, _ -> ()
+            | State id1, Some id2 when Stateid.newer_than id2 id1 -> ()
+            | _ -> Queue.add msg feedbacks (* Put back into the queue *)
+      end;
+        eat_feedback (n-1)
+    in
+      eat_feedback (Queue.length feedbacks)
 
   method private commit_queue_transaction sentence =
     (* A queued command has been successfully done, we push it to [cmd_stack].
        We reget the iters here because Gtk is unable to warranty that they
        were not modified meanwhile. Not really necessary but who knows... *)
     self#mark_as_needed sentence;
-    let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
     buffer#move_mark ~where:stop (`NAME "start_of_input");
-    buffer#remove_tag Tags.Script.to_process ~start ~stop
 
-  method private process_error queue phrase loc msg =
+  method private position_error_tag_at_iter iter phrase = function
+    | None -> ()
+    | Some (start, stop) ->
+        buffer#apply_tag Tags.Script.error
+          ~start:(iter#forward_chars (byte_offset_to_char_offset phrase start))
+          ~stop:(iter#forward_chars (byte_offset_to_char_offset phrase stop))
+
+  method private position_error_tag_at_sentence sentence loc =
+    let start, _, phrase = self#get_sentence sentence in
+    self#position_error_tag_at_iter start phrase loc
+
+  method private process_interp_error queue sentence loc msg id =
     Coq.bind (Coq.return ()) (function () ->
-    let position_error = function
-      | None -> ()
-      | Some (start, stop) ->
-        let soi = self#get_start_of_input in
-        let start =
-          soi#forward_chars (byte_offset_to_char_offset phrase start) in
-        let stop =
-          soi#forward_chars (byte_offset_to_char_offset phrase stop) in
-        buffer#apply_tag Tags.Script.error ~start ~stop;
-        buffer#place_cursor ~where:start
-    in
-    let sentence = Stack.pop cmd_stack in
-    let start = buffer#get_iter_at_mark sentence.start in
-    let stop = buffer#get_iter_at_mark sentence.stop in
+    let start, stop, phrase = self#get_sentence sentence in
     buffer#remove_tag Tags.Script.to_process ~start ~stop;
     self#discard_command_queue queue;
     pop_info ();
-    position_error loc;
+    self#position_error_tag_at_iter start phrase loc;
+    buffer#place_cursor ~where:start;
     messages#clear;
-    messages#push Interface.Error msg;
+    messages#push Error msg;
     self#show_goals)
 
+  method private get_sentence sentence =
+    let start = buffer#get_iter_at_mark sentence.start in
+    let stop = buffer#get_iter_at_mark sentence.stop in
+    let phrase = start#get_slice ~stop in
+    start, stop, phrase
+
   (** Compute the phrases until [until] returns [true]. *)
   method private process_until until verbose =
     let push_msg lvl msg = if verbose then messages#push lvl msg in
@@ -256,29 +339,40 @@ object(self)
         self#show_goals
       else
         let sentence = Queue.pop queue in
-        Stack.push sentence cmd_stack;
+        add_flag sentence `PROCESSING;
+        Searchstack.push sentence cmd_stack;
         if List.mem `COMMENT sentence.flags then
           (self#commit_queue_transaction sentence; loop ())
         else
           (* If the line is not a comment, we interpret it. *)
-          let phrase =
-            let start = buffer#get_iter_at_mark sentence.start in
-            let stop = buffer#get_iter_at_mark sentence.stop in
-            start#get_slice ~stop
-          in
+          let _, _, phrase = self#get_sentence sentence in
           let commit_and_continue msg =
-            push_msg Interface.Notice msg;
+            push_msg Notice msg;
             self#commit_queue_transaction sentence;
             loop ()
           in
-          let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
+          let query =
+            Coq.interp ~logger:push_msg ~verbose sentence.edit_id phrase in
           let next = function
-          | Interface.Good msg -> commit_and_continue msg
-          | Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
+          | Good (id, msg) ->
+              assign_state_id sentence id;
+              commit_and_continue msg
+          | Fail (id, loc, msg) ->
+              let sentence = Searchstack.pop cmd_stack in
+              self#process_interp_error queue sentence loc msg id
           in
           Coq.bind query next
     in
     loop ())
+  
+  method join_document =
+   let next = function
+     | Good _ ->
+         messages#clear;
+         messages#push Info "Document checked";
+         Coq.return ()
+     | Fail x -> self#handle_failure x in
+   Coq.bind (Coq.status ~logger:messages#push true) next
 
   method process_next_phrase =
     let until len start stop = 1 <= len in
@@ -297,94 +391,76 @@ object(self)
   method process_until_end_or_error =
     self#process_until_iter buffer#end_iter
 
-  (** Clear the command stack until [until] returns [true].
-      Returns the number of commands sent to Coqtop to backtrack. *)
-  method private prepare_clear_zone until zone =
-    let merge_zone phrase zone =
-      match zone with
-        | None -> Some (phrase.start, phrase.stop)
-        | Some (start,stop) ->
-          (* phrase should be just before the current clear zone *)
-          buffer#delete_mark phrase.stop;
-          buffer#delete_mark start;
-          Some (phrase.start, stop)
-    in
-    let rec loop len real_len zone =
-      if Stack.is_empty cmd_stack then real_len, zone
-      else
-        let phrase = Stack.top cmd_stack in
-        let is_comment = List.mem `COMMENT phrase.flags in
-        if until len real_len phrase.start phrase.stop then
-          real_len, zone
-        else
-          (* [until] has not been reached, so we'll clear this command *)
-          let _ = Stack.pop cmd_stack in
-          let zone = merge_zone phrase zone in
-          loop (succ len) (if is_comment then real_len else succ real_len) zone
-    in
-    loop 0 0 zone
-
-  method private commit_clear_zone = function
-    | None -> ()
-    | Some (start_mark, stop_mark) ->
-      let start = buffer#get_iter_at_mark start_mark in
-      let stop = buffer#get_iter_at_mark stop_mark in
-      buffer#remove_tag Tags.Script.processed ~start ~stop;
-      buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-      buffer#remove_tag Tags.Script.tooltip ~start ~stop;
-      buffer#move_mark ~where:start (`NAME "start_of_input");
-      buffer#delete_mark start_mark;
-      buffer#delete_mark stop_mark
-
-  (** Actually performs the undoing *)
-  method private undo_command_stack n clear_zone =
-    let next = function
-    | Interface.Good n ->
-      let until _ len _ _ = n <= len in
-      (* Coqtop requested [n] more ACTUAL backtrack *)
-      let _, zone = self#prepare_clear_zone until clear_zone in
-      self#commit_clear_zone zone;
-      Coq.return ()
-    | Interface.Fail (l, str) ->
-      messages#set
-        ("Error while backtracking: " ^ str ^
-          "\nCoqIDE and coqtop may be out of sync," ^
-          "you may want to use Restart.");
-      Coq.return ()
-    in
-    Coq.bind (Coq.rewind n) next
+  method private segment_to_be_cleared until =
+    let finder (n, found, zone) ({ start; stop; state_id } as sentence) =
+      let found = found || until n state_id start stop in
+      match found, state_id with
+      | true, Some id -> `Stop (n, id, Some sentence, zone)
+      | _ -> `Cont (n + 1, found, sentence :: zone) in
+    try Searchstack.find finder (0, false, []) cmd_stack
+    with Not_found ->
+      Searchstack.length cmd_stack, initial_state,
+      None, List.rev (Searchstack.to_list cmd_stack)
 
   (** Wrapper around the raw undo command *)
   method private backtrack_until until =
-    let action () = 
-      push_info "Coq is undoing";
-      messages#clear
+    let opening () =
+      push_info "Coq is undoing" in
+    let conclusion () =
+      pop_info ();
+      buffer#place_cursor ~where:self#get_start_of_input;
+      self#show_goals in
+    let cleanup n l =
+      for i = 1 to n do ignore(Searchstack.pop cmd_stack) done;
+      if l <> [] then begin
+        let start = buffer#get_iter_at_mark (CList.hd l).start in
+        let stop = buffer#get_iter_at_mark (CList.last l).stop in
+        buffer#remove_tag Tags.Script.processed ~start ~stop;
+        buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+(*         buffer#remove_tag Tags.Script.tooltip ~start ~stop; *)
+        buffer#remove_tag Tags.Script.to_process ~start ~stop;
+        buffer#move_mark ~where:start (`NAME "start_of_input")
+      end;
+      List.iter (fun { start } -> buffer#delete_mark start) l;
+      List.iter (fun { stop } -> buffer#delete_mark stop) l in
+    Coq.bind (Coq.lift opening) (fun () ->
+    let rec undo until =
+      let n, to_id, sentence, seg = self#segment_to_be_cleared until in
+      Coq.bind (Coq.backto to_id) (function
+      | Good () -> cleanup n seg; conclusion ()
+      | Fail (safe_id, loc, msg) ->
+          if loc <> None then messages#push Error "Fixme LOC";
+          messages#push Error msg;
+          undo (fun _ id _ _ -> id = Some safe_id))
     in
-    Coq.bind (Coq.lift action) (fun () ->
-    (* Instead of locking the whole buffer, we now simply remove
-       read-only tags *after* the actual backtrack *)
-      let to_undo, zone = self#prepare_clear_zone until None in
-      let next () = pop_info (); Coq.return () in
-      Coq.bind (self#undo_command_stack to_undo zone) next
-    )
+      undo until)
 
   method private backtrack_to_iter iter =
-    let until _ _ _ stop =
-      iter#compare (buffer#get_iter_at_mark stop) >= 0
-    in
-    Coq.seq (self#backtrack_until until)
-      (* We may have backtracked too much: let's replay *)
-      (self#process_until_iter iter)
+    let until _ _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in
+    self#backtrack_until until
+
+  method handle_failure (safe_id, (loc : (int * int) option), msg) =
+    if loc <> None then messages#push Error "Fixme LOC";
+    messages#clear;
+    messages#push Error msg;
+    ignore(self#process_feedback ());
+    let safe_flags s = s.flags = [ `UNSAFE ] || s.flags = [] in
+    let find_last_safe_id () s =
+      match s.state_id with
+      | Some id when safe_flags s -> `Stop id | _ -> `Cont () in
+    try
+      let last_safe_id = Searchstack.find find_last_safe_id () cmd_stack in
+      self#backtrack_until (fun _ id _ _ -> id = Some last_safe_id)
+    with Not_found -> self#backtrack_until (fun _ id _ _ -> id = Some safe_id)
 
   method backtrack_last_phrase =
-    let until len _ _ _ = 1 <= len in
-    Coq.bind (self#backtrack_until until)
-      (fun () ->
-        buffer#place_cursor ~where:self#get_start_of_input;
-        self#show_goals)
+    let until n _ _ _ = n >= 1 in
+    messages#clear;
+    self#backtrack_until until
 
   method go_to_insert =
     Coq.bind (Coq.return ()) (fun () ->
+    messages#clear;
     let point = self#get_insert in
     if point#compare self#get_start_of_input >= 0
     then self#process_until_iter point
@@ -406,7 +482,7 @@ object(self)
           ~start:(`MARK (buffer#create_mark start))
           ~stop:(`MARK (buffer#create_mark stop))
           [] in
-      Stack.push sentence cmd_stack;
+      Searchstack.push sentence cmd_stack;
       messages#clear;
       self#show_goals
     in
@@ -419,12 +495,12 @@ object(self)
       let action = log "Sending to coq now" in
       let query = Coq.interp ~verbose:false 0 phrase in
       let next = function
-      | Interface.Fail (l, str) ->
+      | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
         messages#add ("Unsuccessfully tried: "^phrase);
         more
-      | Interface.Good msg ->
-        messages#add msg;
+      | Good (_, id) ->
+(*         messages#add msg; *)
         stop Tags.Script.processed
       in
       Coq.bind (Coq.seq action query) next
@@ -440,8 +516,8 @@ object(self)
     let action () =
       if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
       (* clear the stack *)
-      while not (Stack.is_empty cmd_stack) do
-        let phrase = Stack.pop cmd_stack in
+      while not (Searchstack.is_empty cmd_stack) do
+        let phrase = Searchstack.pop cmd_stack in
         buffer#delete_mark phrase.start;
         buffer#delete_mark phrase.stop
       done;
@@ -457,38 +533,36 @@ object(self)
     in
     Coq.seq (Coq.lift action) self#initialize
 
-  method private include_file_dir_in_path =
-    let query f =
+  method initialize =
+    let get_initial_state =
+      let next = function
+      | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
+      | Good id -> initial_state <- id; Coq.return () in
+      Coq.bind (Coq.init ()) next in
+    let add_load_path = match get_filename () with
+    | None -> Coq.return ()
+    | Some f ->
       let dir = Filename.dirname f in
       let loadpath = Coq.inloadpath dir in
       let next = function
-      | Interface.Fail (_, s) ->
+      | Fail (_, _, s) ->
         messages#set
           ("Could not determine lodpath, this might lead to problems:\n"^s);
         Coq.return ()
-      | Interface.Good true -> Coq.return ()
-      | Interface.Good false ->
+      | Good true -> Coq.return ()
+      | Good false ->
         let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-        let cmd = Coq.interp 0 cmd in
+        let cmd = Coq.interp (hidden_edit_id ()) cmd in
         let next = function
-        | Interface.Fail (l, str) ->
+        | Fail (_, l, str) ->
           messages#set ("Couln't add loadpath:\n"^str);
           Coq.return ()
-        | Interface.Good _ ->
-          Coq.return ()
+        | Good (id, _) -> initial_state <- id; Coq.return ()
         in
         Coq.bind cmd next
       in
       Coq.bind loadpath next
     in
-    let next () = match get_filename () with
-    | None -> Coq.return ()
-    | Some f -> query f
-    in
-    Coq.bind (Coq.return ()) next
-
-  method initialize =
-    let next () = Coq.PrintOpt.enforce in
-    Coq.bind self#include_file_dir_in_path next
+    Coq.seq get_initial_state (Coq.seq add_load_path Coq.PrintOpt.enforce)
 
 end
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 48a07f48b..37daaf307 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -19,6 +19,11 @@ object
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
+  method join_document : unit task
+
+  method handle_failure : Interface.handle_exn_rty -> unit task
+  
+  method destroy : unit -> unit
 end
 
 class coqops :
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 94f2a38c9..15a3d250c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -487,12 +487,10 @@ end
 
 (** Callbacks for the Navigation menu *)
 
-let update_status =
+let update_status sn =
   let display msg = pop_info (); push_info msg in
   let next = function
-  | Interface.Fail (l, str) ->
-    display "Oops, problem while fetching coq status.";
-    Coq.return ()
+  | Interface.Fail x -> sn.coqops#handle_failure x
   | Interface.Good status ->
     let path = match status.Interface.status_path with
       | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
@@ -505,7 +503,7 @@ let update_status =
     display ("Ready" ^ path ^ name);
     Coq.return ()
   in
-  Coq.bind Coq.status next
+  Coq.bind (Coq.status ~logger:sn.messages#push false) next
 
 let find_next_occurrence ~backward sn =
   (** go to the next occurrence of the current word, forward or backward *)
@@ -521,7 +519,7 @@ let find_next_occurrence ~backward sn =
 
 let send_to_coq f sn =
   let info () = Minilib.log ("Coq busy, discarding query") in
-  let f = Coq.seq (f sn) update_status in
+  let f = Coq.seq (f sn) (update_status sn) in
   Coq.try_grab sn.coqtop f info
 
 let send_to_coq f = on_current_term (send_to_coq f)
@@ -541,6 +539,7 @@ module Nav = struct
     Minilib.log "User break received";
     Coq.break_coqtop sn.coqtop
   let interrupt = cb_on_current_term interrupt
+  let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
 
 let tactic_wizard_callback l _ =
@@ -720,7 +719,9 @@ let about _ =
     "Bruno Barras";
     "Pierre Corbineau";
     "Julien Narboux";
-    "Hugo Herbelin" ]
+    "Hugo Herbelin";
+    "Enrico Tassi";
+    ]
   in
   dialog#set_name "CoqIDE";
   dialog#set_comments "The Coq Integrated Development Environment";
@@ -1082,6 +1083,9 @@ let build_ui () =
     item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
       ~tooltip:"Next occurence"
       ~accel:(prefs.modifier_for_navigation^"greater");
+    item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
+      ~tooltip:"Force the processing of the whole document" 
+      ~accel:(current.modifier_for_navigation^"f"); 
   ];
 
   let tacitem s sc =
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 6b9517a84..fd5bc6c49 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -153,6 +153,7 @@ let init () =
   <toolitem action='Go to' />
   <toolitem action='Start' />
   <toolitem action='End' />
+  <toolitem action='Force' />
   <toolitem action='Interrupt' />
   <toolitem action='Previous' />
   <toolitem action='Next' />
diff --git a/ide/session.ml b/ide/session.ml
index 46780b275..bed0747f3 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -102,6 +102,7 @@ let set_buffer_handlers buffer script =
     let start = get_start () in
     let stop = buffer#end_iter in
     buffer#remove_tag Tags.Script.error ~start ~stop;
+    buffer#remove_tag Tags.Script.error_bg ~start ~stop;
     buffer#remove_tag Tags.Script.tooltip ~start ~stop
   in
   let end_action_cb () =
@@ -152,7 +153,7 @@ let create file coqtop_args =
   let _ = set_buffer_handlers (buffer :> GText.buffer) script in
   let proof = create_proof () in
   let messages = create_messages () in
-  let command = new Wg_Command.command_window coqtop in
+  let command = new Wg_Command.command_window coqtop ~mark_as_broken:(fun _ -> ()) ~mark_as_processed:(fun _ -> ()) ~cur_state:(fun () -> Obj.magic 0) in
   let finder = new Wg_Find.finder (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in
@@ -177,6 +178,7 @@ let kill (sn:session) =
   (* To close the detached views of this script, we call manually
      [destroy] on it, triggering some callbacks in [detach_view].
      In a more modern lablgtk, rather use the page-removed signal ? *)
+  sn.coqops#destroy ();
   sn.script#destroy ();
   Coq.close_coqtop sn.coqtop
 
diff --git a/ide/tags.ml b/ide/tags.ml
index 9af54831f..e668616bf 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -21,6 +21,7 @@ struct
   let table = GText.tag_table ()
   let comment_sentence = make_tag table ~name:"comment_sentence" []
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
+  let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND "#FFCCCC"]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
   let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false]
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold";`EDITABLE false]
@@ -28,7 +29,7 @@ struct
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
   let all =
-    [comment_sentence; error; to_process; processed; unjustified;
+     [comment_sentence; error; error_bg; to_process; processed; unjustified;
      found; sentence; tooltip]
 end
 module Proof =
diff --git a/ide/tags.mli b/ide/tags.mli
index d86dcbc44..ddd240d2a 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -11,6 +11,7 @@ sig
   val table : GText.tag_table
   val comment_sentence : GText.tag
   val error : GText.tag
+  val error_bg : GText.tag
   val to_process : GText.tag
   val processed : GText.tag
   val unjustified : GText.tag
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index ec759b67f..a95b9f892 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -8,7 +8,9 @@
 
 open Preferences
 
-class command_window coqtop =
+class command_window coqtop
+  ~mark_as_broken ~mark_as_processed ~cur_state
+=
 (*  let window = GWindow.window
 		 ~allow_grow:true ~allow_shrink:true
 		 ~width:500 ~height:250
@@ -114,14 +116,14 @@ object(self)
       let log level message = result#buffer#insert (message^"\n") in
       let process =
 	Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
-          | Interface.Fail (l,str) ->
-            result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
+          | Interface.Fail (_,l,str) ->
+            result#buffer#insert str;
 	    Coq.return ()
-          | Interface.Good res ->
-            result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
+          | Interface.Good (_,res) ->
+            result#buffer#insert res; 
 	    Coq.return ())
       in
-      result#buffer#set_text "";
+      result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
       Coq.try_grab coqtop process ignore
     in
     ignore (combo#entry#connect#activate ~callback:(on_activate callback));
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index 3127d38e6..1c5a1e424 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -7,6 +7,9 @@
 (************************************************************************)
 
 class command_window : Coq.coqtop ->
+    mark_as_broken:(Stateid.state_id list -> unit) ->
+    mark_as_processed:(Stateid.state_id list -> unit) ->
+    cur_state:(unit -> Stateid.state_id) ->
   object
     method new_command : ?command:string -> ?term:string -> unit -> unit
     method frame : GBin.frame
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 13c3d4cdb..f58cdc647 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -47,8 +47,10 @@ let message_view () : message_view =
       | Interface.Warning -> [Tags.Message.warning]
       | _ -> []
       in
-      buffer#insert ~tags msg;
-      buffer#insert ~tags "\n"
+      if msg <> "" then begin
+        buffer#insert ~tags msg;
+        buffer#insert ~tags "\n"
+      end
 
     method add msg = self#push Interface.Notice msg
 
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
 
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
index f9b29ca18..49169eba8 100644
--- a/test-suite/ide/undo012.fake
+++ b/test-suite/ide/undo012.fake
@@ -22,5 +22,5 @@ REWIND 1
 # We should now be just before aa, without opened proofs
 INTERPRAW Fail idtac.
 INTERPRAW Fail Check aa.
-INTERPRAW Fail Check bb.
-INTERPRAW Fail Check cc.
+INTERPRAW Check bb.
+INTERPRAW Check cc.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index 3b1c61e66..389da2765 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -20,9 +20,6 @@ INTERP apply H.
 REWIND 2
 # We should now be just before "Lemma cc"
 # <replay>
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
 INTERP Qed.
 INTERP apply H.
 # </replay>
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index 2a6e512cb..a188e31b1 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -18,8 +18,6 @@ INTERP destruct H.
 REWIND 6
 # We should be just before "Lemma bb"
 # <replay>
-INTERP Lemma bb : False -> False.
-INTERP intro H.
 INTERP apply H.
 INTERP Qed.
 INTERP apply H.
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 821830203..65b446ca0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -113,9 +113,9 @@ let coqide_cmd_checks (loc,ast) =
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
 let interp (id,raw,verbosely,s) =
-  Pp.set_id_for_feedback id;
+  set_id_for_feedback (Interface.Edit id);
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let loc_ast = Vernac.parse_sentence (pa,None) in
+  let loc, ast as loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
   Flags.make_silent (not verbosely);
   if id = 0 then Vernac.eval_expr (loc, VernacStm (Command ast))
@@ -191,6 +191,9 @@ let process_goal sigma g =
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let goals () =
+  Stm.finish ();
+  let s = read_stdout () in
+  if s <> "" then msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     let (goals, zipper, sigma) = Proof.proof pfts in
@@ -206,6 +209,9 @@ let goals () =
 
 let evars () =
   try
+    Stm.finish ();
+    let s = read_stdout () in
+    if s <> "" then msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evarutil.non_instantiated sigma in
@@ -228,15 +234,20 @@ let hints () =
       Some (hint_hyps, hint_goal)
   with Proof_global.NoCurrentProof -> None
 
+
 (** Other API calls *)
 
 let inloadpath dir =
   Loadpath.is_in_load_paths (CUnix.physical_path_of_string dir)
 
-let status () =
+let status force =
   (** We remove the initial part of the current [DirPath.t]
       (usually Top in an interactive session, cf "coqtop -top"),
       and display the other parts (opened sections and modules) *)
+  Stm.finish ();
+  if force then Stm.join ();
+  let s = read_stdout () in
+  if s <> "" then msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -253,7 +264,6 @@ let status () =
     Interface.status_path = path;
     Interface.status_proofname = proof;
     Interface.status_allproofs = allproofs;
-    Interface.status_statenum = Lib.current_command_label ();
     Interface.status_proofnum = Stm.current_proof_depth ();
   }
 
@@ -272,6 +282,8 @@ let set_options options =
   in
   List.iter iter options
 
+let mkcases s = Vernacentries.make_cases s
+
 let about () = {
   Interface.coqtop_version = Coq_config.version;
   Interface.protocol_version = Serialize.protocol_version;
@@ -288,7 +300,16 @@ let handle_exn e =
   match e with
   | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
   | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
-  | e -> dummy, loc_of e, mk_msg e
+  | e ->
+      match Stateid.get_state_id e with
+      | Some (valid, _) -> valid, loc_of e, mk_msg e
+      | None -> dummy, loc_of e, mk_msg e
+
+let init =
+  let initialized = ref false in
+  fun () ->
+   if !initialized then anomaly (str "Already initialized")
+   else (initialized := true; Stm.get_current_state ())
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
@@ -298,29 +319,19 @@ let quit = ref false
 
 (** Grouping all call handlers together + error handling *)
 
-let eval_call c =
-  let handle_exn e =
-    catch_break := false;
-    match e with
-      | Errors.Drop -> None, "Drop is not allowed by coqide!"
-      | Errors.Quit -> None, "Quit is not allowed by coqide!"
-      | e ->
-        let loc = match Loc.get_loc e with
-          | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
-          | _ -> None
-        in
-        loc, (read_stdout ())^"\n"^(string_of_ppcmds (Errors.print e))
-  in
+let eval_call xml_oc log c =
   let interruptible f x =
     catch_break := true;
     Util.check_for_interrupt ();
     let r = f x in
     catch_break := false;
+    let out = read_stdout () in
+    if out <> "" then log (str out);
     r
   in
   let handler = {
     Interface.interp = interruptible interp;
-    Interface.rewind = interruptible (fun _ -> 0);
+    Interface.backto = interruptible backto;
     Interface.goals = interruptible goals;
     Interface.evars = interruptible evars;
     Interface.hints = interruptible hints;
@@ -331,28 +342,35 @@ let eval_call c =
     Interface.set_options = interruptible set_options;
     Interface.mkcases = interruptible Vernacentries.make_cases;
     Interface.quit = (fun () -> quit := true);
+    Interface.init = interruptible init;
     Interface.about = interruptible about;
     Interface.handle_exn = handle_exn; }
   in
-  (* If the messages of last command are still there, we remove them *)
-  ignore (read_stdout ());
   Serialize.abstract_eval_call handler c
 
 (** Message dispatching. *)
+let print_xml =
+  let m = Mutex.create () in
+  fun oc xml ->
+    Mutex.lock m;
+    try Xml_printer.print oc xml; Mutex.unlock m
+    with e -> let e = Errors.push e in Mutex.unlock m; raise e
+  
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = Pp.string_of_ppcmds (hov 0 message) in
+  let msg = string_of_ppcmds (hov 0 message) in
   let message = {
     Interface.message_level = level;
     Interface.message_content = msg;
   } in
+  let () = pr_debug (Printf.sprintf "-> %S" msg) in
   let xml = Serialize.of_message message in
-  Xml_printer.print xml_oc xml
+  print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
   let xml = Serialize.of_feedback msg in
-  Xml_printer.print xml_oc xml
+  print_xml xml_oc xml
 
 (** The main loop *)
 
@@ -366,8 +384,8 @@ let loop () =
   let xml_oc = Xml_printer.make (Xml_printer.TChannel !orig_stdout) in
   let xml_ic = Xml_parser.make (Xml_parser.SChannel stdin) in
   let () = Xml_parser.check_eof xml_ic false in
-  Pp.set_logger (slave_logger xml_oc);
-  Pp.set_feeder (slave_feeder xml_oc);
+  set_logger (slave_logger xml_oc);
+  set_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -377,9 +395,9 @@ let loop () =
       let xml_query = Xml_parser.parse xml_ic in
       let q = Serialize.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call q in
+      let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in
       let () = pr_debug_answer q r in
-      Xml_printer.print xml_oc (Serialize.of_answer q r);
+      print_xml xml_oc (Serialize.of_answer q r);
       flush !orig_stdout
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 004ac9428..a6d120d5c 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -402,6 +402,9 @@ end = struct (* {{{ *)
   let freeze id = VCS.set_state id (freeze_global_state ())
 
   let exn_on id ?valid e =
+    let loc = Option.default Loc.ghost (Loc.get_loc e) in
+    let msg = string_of_ppcmds (print e) in
+    Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
     Stateid.add_state_id e ?valid id
 
   let define ?(cache=false) f id =