From c7d2cdb733f71f11ba9923d967d7b630958dfc83 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Sep 2011 16:47:26 +0000 Subject: 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 --- library/lib.ml | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) (limited to 'library/lib.ml') 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. *) -- cgit v1.2.3