diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 15 | ||||
| -rw-r--r-- | library/lib.mli | 3 |
2 files changed, 18 insertions, 0 deletions
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) *) |