CoqIDE ported to the revides protocol

- the zone to be edited is now between the marks
  start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
  a focused zone

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

9 files changed, 296 insertions, 130 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index be35ebe1a..96a19f317 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -370,7 +370,7 @@ let handle_final_answer handle xml =
     | 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) }
+  with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) }
 
 type input_state = {
   mutable fragment : string;
@@ -558,9 +558,9 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s =
-  eval_call ~logger (Serialize.interp (i,raw,verbose,s))
-let backto i = eval_call (Serialize.backto i)
+let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x)
+let edit_at i = eval_call (Serialize.edit_at i)
+let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
 let status ?logger force = eval_call ?logger (Serialize.status force)
diff --git a/ide/coq.mli b/ide/coq.mli
index 330cc776f..4fe6a2188 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -122,13 +122,13 @@ 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 ->
-  ?raw:bool ->
-  ?verbose:bool ->
-    Interface.edit_id -> string           -> Interface.interp_rty query
-val backto     : Interface.backto_sty     -> Interface.backto_rty query
+val add        : ?logger:Ideutils.logger ->
+                 Interface.add_sty        -> Interface.add_rty query
+val edit_at    : Interface.edit_at_sty    -> Interface.edit_at_rty query
+val query      : ?logger:Ideutils.logger ->
+                 Interface.query_sty      -> Interface.query_rty query
 val status     : ?logger:Ideutils.logger ->
-                 Interface.status_sty -> Interface.status_rty query
+                 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
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 081cf62d4..1deb0a8ba 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -16,6 +16,11 @@ type mem_flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ]
 let mem_flag_of_flag : flag -> mem_flag = function
   | `ERROR _ -> `ERROR
   | (`COMMENT | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
+let str_of_flag = function
+  | `COMMENT -> "C"
+  | `UNSAFE -> "U"
+  | `PROCESSING -> "P"
+  | `ERROR _ -> "E"
 
 module SentenceId : sig
 
@@ -38,6 +43,8 @@ module SentenceId : sig
   val same_sentence : sentence -> sentence -> bool
   val hidden_edit_id : unit -> int
 
+  val dbg_to_string : GText.buffer -> sentence -> string
+
 end = struct
 
   type sentence = {
@@ -67,9 +74,24 @@ end = struct
   let has_flag s mf =
     List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
   let remove_flag s mf =
-    s.flags <- List.filter (fun f -> mem_flag_of_flag f = mf) s.flags
+    s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags
   let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id
 
+  let dbg_to_string (b : GText.buffer) s =
+    let ellipsize s =
+            Str.global_replace (Str.regexp "^[\n ]*") ""
+        (if String.length s > 20 then String.sub s 0 17 ^ "..."
+         else s) in
+    Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s]"
+      s.edit_id
+      (Stateid.to_string (Option.default Stateid.dummy s.state_id))
+      (b#get_iter_at_mark s.start)#offset
+      (b#get_iter_at_mark s.stop)#offset
+      (ellipsize
+        ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+      (String.concat "," (List.map str_of_flag s.flags))
+
+
 end
 open SentenceId
 
@@ -132,8 +154,54 @@ object(self)
   method destroy () =
     feedback_timer.Ideutils.kill ()
 
+  method private print_stack =
+    Minilib.log "cmd_stack:";
+    let top, mid, bot = Stack.to_lists cmd_stack in
+    Minilib.log "--start--";
+    List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) top;
+    if Stack.focused cmd_stack then Minilib.log "----";
+    List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) mid;
+    if Stack.focused cmd_stack then Minilib.log "----";
+    List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) bot;
+    Minilib.log "--stop--"
+
+  method private enter_focus start stop to_id tip =
+    if Stack.focused cmd_stack then begin
+      self#exit_focus tip
+    end;
+    let at id s = s.state_id = Some id in
+    self#print_stack;
+    Minilib.log("Focusing "^Stateid.to_string start^" "^Stateid.to_string stop);
+    Stack.focus cmd_stack ~cond_top:(at start) ~cond_bot:(at stop);
+    self#print_stack;
+    let qed_s = Stack.top cmd_stack in
+    buffer#apply_tag Tags.Script.read_only
+      ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char
+        (fun c -> not(Glib.Unichar.isspace c)))
+      ~stop:(buffer#get_iter_at_mark qed_s.stop);
+    buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
+      (`NAME "stop_of_input")
+
+  method private exit_focus newtip =
+    self#print_stack;
+    Minilib.log "Unfocusing";
+    Stack.unfocus cmd_stack;
+    self#print_stack;
+    if (Some newtip <> (Stack.top cmd_stack).state_id) then begin
+      Minilib.log ("Cutting tip to " ^ Stateid.to_string newtip);
+      let until _ id _ _ = id = Some newtip in
+      let n, _, _, seg = self#segment_to_be_cleared until in
+      self#cleanup n seg
+    end;
+    let where = buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
+    buffer#move_mark ~where (`NAME "start_of_input");
+    buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input")
+
   method private get_start_of_input =
     buffer#get_iter_at_mark (`NAME "start_of_input")
+  
+  method private get_end_of_input =
+    buffer#get_iter_at_mark (`NAME "stop_of_input")
 
   method private get_insert =
     buffer#get_iter_at_mark `INSERT
@@ -162,56 +230,23 @@ object(self)
       else messages#add s;
     in
     let query =
-      Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
+      Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
     let next = function
-    | Fail (_, _, err) -> display_error err; Coq.return () (* XXX*)
-    | Good (_, msg) ->
+    | Fail (_, _, err) -> display_error err; Coq.return ()
+    | Good msg ->
       messages#add msg; Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
 
-  (** [fill_command_queue until q] fills a command queue until the [until]
-      condition returns true; it is fed with the number of phrases read and the
-      iters enclosing the current sentence. *)
-  method private fill_command_queue until queue =
-    let rec loop len iter =
-      match Sentence.find buffer iter with
-      | None -> raise Exit
-      | Some (start, stop) ->
-        if until len start stop then raise Exit;
-        buffer#apply_tag Tags.Script.to_process ~start ~stop;
-        (* Check if this is a comment *)
-        let is_comment =
-          stop#backward_char#has_tag Tags.Script.comment_sentence
-        in
-        let sentence =
-          mk_sentence
-            ~start:(`MARK (buffer#create_mark start))
-            ~stop:(`MARK (buffer#create_mark stop))
-            (if is_comment then [`COMMENT] else []) in
-        Queue.push sentence queue;
-        if not stop#is_end then loop (succ len) stop
-    in
-    try loop 0 self#get_start_of_input with Exit -> ()
-
-  method private discard_command_queue queue =
-    while not (Queue.is_empty queue) do
-      let sentence = Queue.pop queue in
-      let start = buffer#get_iter_at_mark sentence.start in
-      let stop = buffer#get_iter_at_mark sentence.stop in
-      buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      buffer#delete_mark sentence.start;
-      buffer#delete_mark sentence.stop;
-    done
-
   method private mark_as_needed sentence =
+    Minilib.log("Marking " ^ dbg_to_string buffer sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
     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 all_tags = [ error_bg; to_process; processed; unjustified ] in
     let tags =
       (if has_flag sentence `PROCESSING then to_process else
        if has_flag sentence `ERROR then error_bg else
@@ -326,7 +361,7 @@ object(self)
     self#discard_command_queue queue;
     pop_info ();
     self#position_error_tag_at_iter start phrase loc;
-    buffer#place_cursor ~where:start;
+    buffer#place_cursor ~where:stop;
     messages#clear;
     messages#push Error msg;
     self#show_goals)
@@ -337,6 +372,48 @@ object(self)
     let phrase = start#get_slice ~stop in
     start, stop, phrase
 
+  (** [fill_command_queue until q] fills a command queue until the [until]
+      condition returns true; it is fed with the number of phrases read and the
+      iters enclosing the current sentence. *)
+  method private fill_command_queue until queue =
+    let rec loop len iter =
+      match Sentence.find buffer iter with
+      | None -> ()
+      | Some (start, stop) ->
+        if until len start stop then begin
+          ()
+        end else if start#has_tag Tags.Script.processed then begin
+          Queue.push (`Skip (start, stop)) queue;
+          loop len stop
+        end else begin
+          buffer#apply_tag Tags.Script.to_process ~start ~stop;
+          (* Check if this is a comment *)
+          let is_comment =
+            stop#backward_char#has_tag Tags.Script.comment_sentence
+          in
+          let sentence =
+            mk_sentence
+              ~start:(`MARK (buffer#create_mark start))
+              ~stop:(`MARK (buffer#create_mark stop))
+              (if is_comment then [`COMMENT] else []) in
+          Queue.push (`Sentence sentence) queue;
+          if not stop#is_end then loop (succ len) stop
+        end
+    in
+    loop 0 self#get_start_of_input
+
+  method private discard_command_queue queue =
+    while not (Queue.is_empty queue) do
+      match Queue.pop queue with
+      | `Skip _ -> ()
+      | `Sentence sentence ->
+          let start = buffer#get_iter_at_mark sentence.start in
+          let stop = buffer#get_iter_at_mark sentence.stop in
+          buffer#remove_tag Tags.Script.to_process ~start ~stop;
+          buffer#delete_mark sentence.start;
+          buffer#delete_mark sentence.stop;
+    done
+
   (** 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
@@ -353,41 +430,59 @@ object(self)
       Minilib.log "Begin command processing";
       queue)
     in
+    let tip =
+      try Stack.fold_until (fun () -> function
+          | { state_id = Some id } -> Stop id
+          | _ -> Next ()) () cmd_stack
+      with Not_found -> initial_state in
     Coq.bind action (fun queue ->
-    let rec loop () =
+    let rec loop tip topstack =
       if Queue.is_empty queue then
         let () = pop_info () in
         let () = script#recenter_insert in
-        self#show_goals
+        match topstack with
+        | [] -> self#show_goals
+        | s :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start)
       else
-        let sentence = Queue.pop queue in
+        match Queue.pop queue, topstack with
+        | `Skip(start,stop), [] -> assert false
+        | `Skip(start,stop), s :: topstack ->
+            assert(start#equal (buffer#get_iter_at_mark s.start));
+            assert(stop#equal (buffer#get_iter_at_mark s.stop));
+            loop tip topstack
+        | `Sentence sentence, _ :: _ -> assert false
+        | `Sentence sentence, [] ->
         add_flag sentence `PROCESSING;
         Stack.push sentence cmd_stack;
         if has_flag sentence `COMMENT then
           let () = remove_flag sentence `PROCESSING in
           let () = self#commit_queue_transaction sentence in
-          loop ()
+          loop tip topstack
         else
           (* If the line is not a comment, we interpret it. *)
           let _, _, phrase = self#get_sentence sentence in
-          let commit_and_continue msg =
-            push_msg Notice msg;
-            self#commit_queue_transaction sentence;
-            loop ()
-          in
           let query =
-            Coq.interp ~logger:push_msg ~verbose sentence.edit_id phrase in
+            Coq.add ~logger:push_msg ((phrase,sentence.edit_id),(tip,verbose))in
           let next = function
-          | Good (id, msg) ->
+          | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
+              assign_state_id sentence id;
+              push_msg Notice msg;
+              self#commit_queue_transaction sentence;
+              loop id []
+          | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
               assign_state_id sentence id;
-              commit_and_continue msg
+              let topstack, _, _ = Stack.to_lists cmd_stack in
+              self#exit_focus tip;
+              push_msg Notice msg;
+              self#mark_as_needed sentence;
+              loop tip (List.rev topstack)
           | Fail (id, loc, msg) ->
               let sentence = Stack.pop cmd_stack in
               self#process_interp_error queue sentence loc msg id
           in
           Coq.bind query next
     in
-    loop ())
+    loop tip [])
   
   method join_document =
    let next = function
@@ -430,7 +525,7 @@ object(self)
     self#process_until until false
 
   method process_until_end_or_error =
-    self#process_until_iter buffer#end_iter
+    self#process_until_iter self#get_end_of_input
 
   method private segment_to_be_cleared until =
     let finder (n, found, zone) ({ start; stop; state_id } as sentence) =
@@ -438,11 +533,29 @@ object(self)
       match found, state_id with
       | true, Some id -> Stop (n, id, Some sentence, zone)
       | _ -> Next (n + 1, found, sentence :: zone) in
-    try Stack.seek finder (0, false, []) cmd_stack
+    try Stack.fold_until finder (0, false, []) cmd_stack
     with Not_found ->
+            Minilib.log "ALL";
       Stack.length cmd_stack, initial_state,
       None, List.rev (Stack.to_list cmd_stack)
 
+  method private cleanup n seg =
+    Minilib.log("Clean "^string_of_int n^" "^string_of_int(List.length seg));
+    for i = 1 to n do ignore(Stack.pop cmd_stack) done;
+    if seg <> [] then begin
+      let start = buffer#get_iter_at_mark (CList.hd seg).start in
+      let stop = buffer#get_iter_at_mark (CList.last seg).stop in
+      Minilib.log("Clean tags in range "^string_of_int start#offset^
+        " "^string_of_int stop#offset);
+      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) seg;
+    List.iter (fun { stop } -> buffer#delete_mark stop) seg
+
   (** Wrapper around the raw undo command *)
   method private backtrack_until ?(move_insert=true) until =
     let opening () =
@@ -450,25 +563,28 @@ object(self)
     let conclusion () =
       pop_info ();
       if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+      let start = self#get_start_of_input in
+      let stop = self#get_end_of_input in
+      Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
+      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;
+      buffer#remove_tag Tags.Script.processed ~start ~stop;
+      buffer#remove_tag Tags.Script.to_process ~start ~stop;
       self#show_goals in
-    let cleanup n l =
-      for i = 1 to n do ignore(Stack.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 ()
+      Coq.bind (Coq.edit_at to_id) (function
+      | Good (CSig.Inl (* NewTip *) ()) ->
+          self#cleanup n seg;
+          conclusion ()
+      | Good (CSig.Inr (* Focus  *) (stop_id,(start_id,tip))) ->
+          self#enter_focus start_id stop_id to_id tip;
+          let n, to_id, sentence, seg =
+            self#segment_to_be_cleared (fun _ id _ _ -> id = Some to_id) in
+          self#cleanup n seg;
+          conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Error "Fixme LOC";
           messages#push Error msg;
@@ -485,14 +601,7 @@ object(self)
     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 -> safe_flags s | None -> false in
-    try
-      let last_safe = Stack.find find_last_safe_id cmd_stack in
-      self#backtrack_until (fun _ id _ _ -> id = last_safe.state_id)
-    with Not_found -> self#backtrack_until (fun _ id _ _ -> id = Some safe_id)
+    self#backtrack_until ~move_insert:false (fun _ id _ _ -> id = Some safe_id)
 
   method backtrack_last_phrase =
     let until n _ _ _ = n >= 1 in
@@ -543,14 +652,14 @@ object(self)
     in
     let try_phrase phrase stop more =
       let action = log "Sending to coq now" in
-      let query = Coq.interp ~verbose:false 0 phrase in
+      let query = Coq.query (phrase,Stateid.dummy) in
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
         messages#add ("Unsuccessfully tried: "^phrase);
         more
-      | Good (_, id) ->
-(*         messages#add msg; *)
+      | Good msg ->
+        messages#add msg;
         stop Tags.Script.processed
       in
       Coq.bind (Coq.seq action query) next
@@ -566,6 +675,7 @@ object(self)
     let action () =
       if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
       (* clear the stack *)
+      if Stack.focused cmd_stack then Stack.unfocus cmd_stack;
       while not (Stack.is_empty cmd_stack) do
         let phrase = Stack.pop cmd_stack in
         buffer#delete_mark phrase.start;
@@ -573,6 +683,7 @@ object(self)
       done;
       (* reset the buffer *)
       buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
+      buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input");
       Sentence.tag_all buffer;
       (* clear the views *)
       messages#clear;
@@ -604,12 +715,13 @@ object(self)
       | Good true -> Coq.return ()
       | Good false ->
         let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-        let cmd = Coq.interp (hidden_edit_id ()) cmd in
+        let cmd = Coq.add ((cmd,hidden_edit_id ()),(Stateid.initial,false)) in
         let next = function
         | Fail (_, l, str) ->
           messages#set ("Couln't add loadpath:\n"^str);
           Coq.return ()
-        | Good (id, _) -> initial_state <- id; Coq.return ()
+        | Good (id, _) ->
+          initial_state <- id; Coq.return ()
         in
         Coq.bind cmd next
       in
diff --git a/ide/sentence.ml b/ide/sentence.ml
index 01add490e..7b98d5296 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -14,7 +14,8 @@
     an unterminated sentence. *)
 
 let split_slice_lax (buffer:GText.buffer) start stop =
-  List.iter (buffer#remove_tag ~start ~stop) Tags.Script.all;
+  buffer#remove_tag ~start ~stop Tags.Script.sentence;
+  buffer#remove_tag ~start ~stop Tags.Script.error;
   let slice = buffer#get_text ~start ~stop () in
   let apply_tag off tag =
     (* off is now a utf8-compliant char offset, cf Coq_lex.utf8_adjust *)
@@ -98,14 +99,16 @@ let tag_on_insert buffer =
            found by [grab_ending_dot] to form a non-ending "..".
          In any case, we retag up to eof, since this isn't that costly. *)
       if not stop#is_end then
-        try split_slice_lax buffer start buffer#end_iter
+        let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in
+        try split_slice_lax buffer start eoi
         with Coq_lex.Unterminated -> ()
   with StartError ->
     buffer#apply_tag ~start:soi ~stop:soi#forward_char Tags.Script.error
 
 let tag_all buffer =
   let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
-  try split_slice_lax buffer soi buffer#end_iter
+  let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in
+  try split_slice_lax buffer soi eoi
   with Coq_lex.Unterminated -> ()
 
 (** Search a sentence around some position *)
diff --git a/ide/session.ml b/ide/session.ml
index e9d4b48ac..837674424 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -35,6 +35,8 @@ let create_buffer () =
     ()
   in
   let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
+  let _ = buffer#create_mark
+    ~left_gravity:false ~name:"stop_of_input" buffer#end_iter in
   let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
   let _ = buffer#place_cursor ~where:buffer#start_iter in
   let _ = buffer#add_selection_clipboard Ideutils.cb in
@@ -93,41 +95,75 @@ let set_buffer_handlers
   let call_coq_or_cancel_action f =
     Coq.try_grab coqtop f (fun () -> cancel_signal "Coq busy") in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
+  let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
+  let ensure_marks_exist () =
+    try ignore(buffer#get_mark (`NAME "stop_of_input"))
+    with GText.No_such_mark _ -> assert false in
   let get_insert () = buffer#get_iter_at_mark `INSERT in
+  let debug_edit_zone () = if !Minilib.debug then begin
+    buffer#remove_tag Tags.Script.edit_zone
+      ~start:buffer#start_iter ~stop:buffer#end_iter;
+    buffer#apply_tag Tags.Script.edit_zone
+      ~start:(get_start()) ~stop:(get_stop())
+    end in
+  let backto_before_error it =
+    let rec aux old it =
+      if it#is_start || not(it#has_tag Tags.Script.error_bg) then old
+      else aux it it#backward_char in
+    aux it it in
   let insert_cb it s = if String.length s = 0 then () else begin
     Minilib.log ("insert_cb " ^ string_of_int it#offset);
     let text_mark = add_mark it in
     if it#has_tag Tags.Script.to_process then
-      cancel_signal "Altering to the script being processed in not implemented"
+      cancel_signal "Altering the script being processed in not implemented"
+    else if it#has_tag Tags.Script.read_only then
+      cancel_signal "Altering read_only text not allowed"
     else if it#has_tag Tags.Script.processed then
       call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
-    end in
+    else if it#has_tag Tags.Script.error_bg then begin
+      let prev_sentence_end = backto_before_error it in
+      let text_mark = add_mark prev_sentence_end in
+      call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+    end end in
   let delete_cb ~start ~stop =
     Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
-    let min_iter = if start#compare stop < 0 then start else stop in
+    cur_action := new_action_id ();
+    let min_iter, max_iter =
+      if start#compare stop < 0 then start, stop else stop, start in
     let text_mark = add_mark min_iter in
-    if min_iter#has_tag Tags.Script.to_process then
-      cancel_signal "Altering to the script being processed in not implemented"
-    else if min_iter#has_tag Tags.Script.processed then
-      call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) in
+    let rec aux min_iter =
+      if min_iter#equal max_iter then ()
+      else if min_iter#has_tag Tags.Script.to_process then
+        cancel_signal "Altering the script being processed in not implemented"
+      else if min_iter#has_tag Tags.Script.read_only then
+        cancel_signal "Altering read_only text not allowed"
+      else if min_iter#has_tag Tags.Script.processed then
+        call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+      else if min_iter#has_tag Tags.Script.error_bg then
+        let prev_sentence_end = backto_before_error min_iter in
+        let text_mark = add_mark prev_sentence_end in
+        call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+      else aux min_iter#forward_char in
+    aux min_iter in
   let begin_action_cb () =
+    Minilib.log "begin_action_cb";
     action_was_cancelled := false;
     let where = get_insert () in
     buffer#move_mark (`NAME "prev_insert") ~where in
   let end_action_cb () =
     Minilib.log "end_action_cb";
+    ensure_marks_exist ();
     if not !action_was_cancelled then begin
-      Minilib.log "cleanup tags";
-      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;
-      buffer#remove_tag Tags.Script.processed ~start ~stop;
-      buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      Sentence.tag_on_insert buffer;
+      Sentence.tag_on_insert buffer
     end in
+  let mark_deleted_cb m =
+    match GtkText.Mark.get_name m with
+    | Some "insert" -> ()
+    | Some s -> Minilib.log (s^" deleted")
+    | None -> ()
+  in
   let mark_set_cb it m =
+    debug_edit_zone ();
     let ins = get_insert () in
     let line = ins#line + 1 in
     let off = ins#line_offset + 1 in
@@ -144,6 +180,7 @@ let set_buffer_handlers
   let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in
   let _ = buffer#connect#end_user_action ~callback:end_action_cb in
   let _ = buffer#connect#after#mark_set ~callback:mark_set_cb in
+  let _ = buffer#connect#after#mark_deleted ~callback:mark_deleted_cb in
   ()
 
 let create_proof () =
diff --git a/ide/tags.ml b/ide/tags.ml
index a91905dcd..de3287720 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -28,9 +28,19 @@ struct
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
+
   let all =
      [comment_sentence; error; error_bg; to_process; processed; unjustified;
      found; sentence; tooltip]
+
+  let edit_zone =
+    let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
+    t#set_priority (List.length all);
+    t
+  let all = edit_zone :: all
+  
+  let read_only = make_tag table ~name:"read_only" [`EDITABLE false ]
+
 end
 module Proof =
 struct
diff --git a/ide/tags.mli b/ide/tags.mli
index ddd240d2a..f79ae1f11 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -18,7 +18,11 @@ sig
   val found : GText.tag
   val sentence : GText.tag
   val tooltip : GText.tag
+  val edit_zone : GText.tag (* for debugging *)
   val all : GText.tag list
+
+  (* Not part of the all list. Special tags! *)
+  val read_only : GText.tag
 end
 
 module Proof :
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index a95b9f892..3422b1682 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -115,11 +115,11 @@ object(self)
       in
       let log level message = result#buffer#insert (message^"\n") in
       let process =
-	Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
+	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
             result#buffer#insert str;
 	    Coq.return ()
-          | Interface.Good (_,res) ->
+          | Interface.Good res ->
             result#buffer#insert res; 
 	    Coq.return ())
       in
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index cbfb3b318..88674545f 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -112,20 +112,17 @@ let coqide_cmd_checks (loc,ast) =
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
-let interp (id,raw,verbosely,s) =
-  set_id_for_feedback (Interface.Edit id);
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) 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 Int.equal id 0 then Vernac.eval_expr (loc, VernacStm (Command ast))
-  else Vernac.eval_expr loc_ast;
-  Flags.make_silent true;
-  Stm.get_current_state (), read_stdout ()
-
-let backto id =
-  Vernac.eval_expr (Loc.ghost,
-    VernacStm (Command (VernacBackTo (Stateid.to_int id))))
+let add ((s,eid),(sid,verbose)) =
+  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in
+  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
+  newid, (rc, read_stdout ())
+
+let edit_at id =
+  match Stm.edit_at id with
+  | `NewTip -> CSig.Inl ()
+  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))
+
+let query (s,id) = Stm.query ~at:id s; read_stdout ()
 
 (** Goal display *)
 
@@ -330,8 +327,9 @@ let eval_call xml_oc log c =
     r
   in
   let handler = {
-    Interface.interp = interruptible interp;
-    Interface.backto = interruptible backto;
+    Interface.add = interruptible add;
+    Interface.edit_at = interruptible edit_at;
+    Interface.query = interruptible query;
     Interface.goals = interruptible goals;
     Interface.evars = interruptible evars;
     Interface.hints = interruptible hints;
@@ -393,10 +391,12 @@ let loop () =
   while not !quit do
     try
       let xml_query = Xml_parser.parse xml_ic in
+(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
       let q = Serialize.to_call xml_query in
       let () = pr_debug_call q in
       let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in
       let () = pr_debug_answer q r in
+(*       pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *)
       print_xml xml_oc (Serialize.of_answer q r);
       flush !orig_stdout
     with