diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 53 | ||||
| -rw-r--r-- | library/lib.mli | 6 |
2 files changed, 38 insertions, 21 deletions
diff --git a/library/lib.ml b/library/lib.ml index 49e685f63..ac710c357 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -150,19 +150,21 @@ let find_split_p p = in find !lib_stk -let split_lib sp = +let split_lib_gen test = let rec collect after equal = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after (hd::equal) before else after,equal,hd::before + | hd::before -> + if test hd then collect after (hd::equal) before else after,equal,hd::before | [] -> after,equal,[] in let rec findeq after = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after [hd] before else findeq (hd::after) before + | hd :: before -> + if test hd then collect after [hd] before else findeq (hd::after) before | [] -> error "no such entry" in findeq [] !lib_stk +let split_lib sp = split_lib_gen (fun x -> (fst x) = sp) + (* Adding operations. *) let add_entry sp node = @@ -491,6 +493,10 @@ let close_section id = (*****************) (* Backtracking. *) +let (inLabel,outLabel) = + declare_object {(default_object "DOT") with + classify_function = (fun _ -> Dispose)} + let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) | (_,OpenedSection _) -> add_section () @@ -501,8 +507,8 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let reset_to sp = - let (_,_,before) = split_lib sp in +let reset_to_gen test = + let (_,_,before) = split_lib_gen test in lib_stk := before; recalc_path_prefix (); let spf = match find_entry_p is_frozen_state with @@ -510,7 +516,10 @@ let reset_to sp = | _ -> assert false in let (after,_,_) = split_lib spf in - recache_context after + let res = recache_context after in + res + +let reset_to sp = reset_to_gen (fun x -> (fst x) = sp) let reset_name (loc,id) = let (sp,_) = @@ -549,10 +558,6 @@ let reset_mod (loc,id) = recache_context after -let (inLabel,outLabel) = - declare_object {(default_object "DOT") with - classify_function = (fun _ -> Dispose)} - let mark_end_of_command, current_command_label, set_command_label = let n = ref 0 in (fun () -> @@ -562,17 +567,23 @@ let mark_end_of_command, current_command_label, set_command_label = (fun () -> !n), (fun x -> n:=x) -let rec reset_label_stk n stk = - match stk with - (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp - | _::tail -> reset_label_stk n tail - | [] -> error "Unknown state number" +let is_label_n n x = + match x with + | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true + | _ -> false +(* Reset the label registered by [mark_end_of_command()] with number n. *) let reset_label n = - let res = reset_label_stk n !lib_stk in - set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) - reset_to res - + let current = current_command_label() in + if n < current then + let res = reset_to_gen (is_label_n n) in + set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) + res + else (* optimisation to avoid recaching when not necessary (why is it so long??) *) + match !lib_stk with + | [] -> () + | x :: ls -> (lib_stk := ls;set_command_label (n-1)) + let rec back_stk n stk = match stk with (sp,Leaf o)::tail when object_tag o = "DOT" -> diff --git a/library/lib.mli b/library/lib.mli index 52e6b7bd7..5639ffed7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -65,8 +65,14 @@ val add_anonymous_leaf : obj -> unit val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit + +(* Adds a "dummy" entry in lib_stk with a unique new label number. *) val mark_end_of_command : unit -> unit +(* Returns the current label number *) val current_command_label : unit -> int +(* [reset_label n ] resets [lib_stk] to the label n registered by + [mark_end_of_command()]. That is it forgets the label and anything + registered after it. *) val reset_label : int -> unit (*s The function [contents_after] returns the current library segment, |