Coqide: new backtracking code, based on the Backtrack command

 This approach, inspired by ProofGeneral, is *much* simplier than earlier,
 and should be more robust (I hope! feedback of testers is welcome).

 Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
 A stack on the coqtop side (in Ide_slave) convert this phrase count to
 labels in the sense of Backtrack, and to abort + depth informations
 concerning proofs.

 We avoid re-entering finished proofs during Rewind by some extra backtracking
 until before these proofs. The amount of extra backtracking is then answered
 by coqtop to coqide. Now:
  - for go_to_insert (the "goto" button), unlike PG, coqide replays
    the extra backtracked zone.
  - for undo_last_step (the "back" button), coqide now leaves the extra
    backtracked zone undone, just like PG. This happens typically when
    undoing a Qed, and this should be the only visible semantical change
    of this patch.

 Two points to check with Pierre C:
  - such a coqtop-side stack mapping labels to opened proofs might be
    interesting to PG, instead of passing lots of info via the prompt and
    computing stuff in emacs.
  - Unlike PG, we allow re-entering inside a module / section, while
    PG retracts to the start of it. Coqide seems to work fine this way, to
    check.

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

2 files changed, 3 insertions, 19 deletions

diff --git a/library/lib.ml b/library/lib.ml
index f6b25e201..cfaea3b66 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -553,13 +553,6 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
-let has_top_frozen_state () =
-  let rec aux = function
-  | (sp, FrozenState _)::_ -> Some sp
-  | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
-  | _ -> None
-  in aux !lib_stk
-
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
@@ -579,14 +572,6 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-let reset_to_state sp =
-  let (_,eq,before) = split_lib sp in
-  (* if eq a frozen state, we'll reset to it *)
-  match eq with
-  | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f
-  | _ -> error "Not a frozen state"
-
-
 (* LEM: TODO
  * We will need to muck with frozen states in after, too!
  * Not only FrozenState, but also those embedded in Opened(Section|Module)
@@ -677,7 +662,9 @@ let rec back_stk n stk =
     | _::tail -> back_stk n tail
     | [] -> error "Reached begin of command history"
 
-let back n = reset_to (back_stk n !lib_stk)
+let back n =
+  reset_to (back_stk n !lib_stk);
+  set_command_label (current_command_label () - n - 1)
 
 (* State and initialization. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 419f91317..0d6eb34b8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -157,9 +157,6 @@ val reset_to : Libnames.object_name -> unit
 val reset_name : Names.identifier Util.located -> unit
 val remove_name : Names.identifier Util.located -> unit
 val reset_mod : Names.identifier Util.located -> unit
-val reset_to_state : Libnames.object_name -> unit
-
-val has_top_frozen_state : unit -> Libnames.object_name option
 
 (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
    [mark_end_of_command] (counting backwards) *)