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

13 files changed, 327 insertions, 244 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index beece54976..718eb718fc 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 27566c6cab..b9b7c1d456 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 ed78e96e28..330cc776f7 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 15ca34b2fa..4105bd82ac 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 48a07f48ba..37daaf3072 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 94f2a38c92..15a3d250c8 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 6b9517a844..fd5bc6c496 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 46780b2757..bed0747f3f 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 9af54831f3..e668616bfb 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 d86dcbc446..ddd240d2a2 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 ec759b67fb..a95b9f8928 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 3127d38e60..1c5a1e424d 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 13c3d4cdbc..f58cdc6477 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