From 9fec60111a49960a01ffdd863d69fea57960edc5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 24 May 2008 14:32:25 +0000
Subject: - Prise en compte des frozen state de Coq autant que possible pour  
 améliorer l'efficacité du undo. Restent les Qed et les End dont le   undo
 peut nécessiter de rejouer un segment arbitrairement complexe   (pour le undo
 du Qed, il faudrait typiquement que Coq se souvienne   de l'entrelacement de
 déclarations et de tactiques). - Code mort concernant les mots-clés dans
 coq.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml  | 15 +++++++++++++++
 library/lib.mli |  3 +++
 2 files changed, 18 insertions(+)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index ae1a41ca13..5e22c4d225 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -584,6 +584,13 @@ 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 ();
@@ -603,6 +610,14 @@ 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;  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|Modtype)
diff --git a/library/lib.mli b/library/lib.mli
index da8ace0481..f3fa9a4b37 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -145,6 +145,9 @@ val reset_to : object_name -> unit
 val reset_name : identifier located -> unit
 val remove_name : identifier located -> unit
 val reset_mod : identifier located -> unit
+val reset_to_state : object_name -> unit
+
+val has_top_frozen_state : unit -> object_name option
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)
-- 
cgit v1.2.3