aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:26 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:26 +0000
commitc7d2cdb733f71f11ba9923d967d7b630958dfc83 (patch)
tree949b5067ece992d6ae6db9e6049ced5801a1a62f /library
parent0692216822e1fd9001f15178c5cb9dd91c9fbc74 (diff)
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
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml19
-rw-r--r--library/lib.mli3
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) *)