diff options
| -rw-r--r-- | library/lib.ml | 33 | ||||
| -rw-r--r-- | library/lib.mli | 1 |
2 files changed, 34 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index c686e2ccf0..985d9efba8 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -140,6 +140,13 @@ let find_entry_p p = in find !lib_stk +let find_split_p p = + let rec find = function + | [] -> raise Not_found + | ent::l -> if p ent then ent,l else find l + in + find !lib_stk + let split_lib sp = let rec collect after equal = function | ((sp',_) as hd)::before -> @@ -432,6 +439,32 @@ let reset_name (loc,id) = in reset_to sp +let is_mod_node = function + | OpenedModule _ | OpenedModtype _ | OpenedSection _ + | ClosedSection _ -> true | _ -> false + +(* Reset on a module or section name in order to bypass constants with + the same name *) + +let reset_mod (loc,id) = + let (ent,before) = + try + find_split_p (fun (sp,node) -> + let (_,spi) = repr_path (fst sp) in id = spi + && is_mod_node node) + with Not_found -> + user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry") + in + lib_stk := before; + recalc_path_prefix (); + let spf = match find_entry_p is_frozen_state with + | (sp, FrozenState f) -> unfreeze_summaries f; sp + | _ -> assert false + in + let (after,_,_) = split_lib spf in + recache_context after + + let point_obj = let (f,_) = declare_object {(default_object "DOT") with classify_function = (fun _ -> Dispose)} in diff --git a/library/lib.mli b/library/lib.mli index 6acb565a8f..2f51d441d9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -128,6 +128,7 @@ val close_section : export:bool -> identifier -> val reset_to : object_name -> unit val reset_name : identifier located -> unit +val reset_mod : identifier located -> unit (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) |