Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 16 insertions, 95 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 7554fd0b..bb3b5716 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -572,72 +572,16 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-(* LEM: TODO
- * We will need to muck with frozen states in after, too!
- * Not only FrozenState, but also those embedded in Opened(Section|Module)
- *)
-let delete_gen test =
-  let (after,equal,before) = split_lib_gen test in
-  let rec chop_at_dot = function
-    | [] as l -> l
-    | (_, Leaf o)::t when object_tag o = "DOT" -> t
-    | _::t -> chop_at_dot t
-  and chop_before_dot = function
-    | [] as l -> l
-    | (_, Leaf o)::t as l when object_tag o = "DOT" -> l
-    | _::t -> chop_before_dot t
- in
-  set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
-
-let delete sp = delete_gen (fun x -> fst x = sp)
-
-let reset_name (loc,id) =
-  let (sp,_) =
-    try
-      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
-    with Not_found ->
-      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
-  in
-  reset_to sp
-
-let remove_name (loc,id) =
-  let (sp,_) =
-    try
-      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
-    with Not_found ->
-      user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
-  in
-    delete sp
+let first_command_label = 1
 
-let is_mod_node = function
-  | OpenedModule _ | OpenedSection _
-  | ClosedModule _ | ClosedSection _  -> true
-  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
-	|| t = "MODULE ALIAS"
-  | _ -> false
-
-(* Reset on a module or section name in order to bypass constants with
-   the same name *)
-
-let reset_mod (loc,id) =
-  let (_,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
-  set_lib_stk before
-
-let mark_end_of_command, current_command_label, set_command_label =
-  let n = ref 0 in
+let mark_end_of_command, current_command_label, reset_command_label =
+  let n = ref (first_command_label-1) in
   (fun () ->
     match !lib_stk with
         (_,Leaf o)::_ when object_tag o = "DOT" -> ()
       | _ -> incr n;add_anonymous_leaf (inLabel !n)),
   (fun () -> !n),
-  (fun x -> n:=x)
+  (fun x -> n:=x;add_anonymous_leaf (inLabel x))
 
 let is_label_n n x =
   match x with
@@ -650,21 +594,21 @@ let is_label_n n x =
 let reset_label n =
   if n >= current_command_label () then
     error "Cannot backtrack to the current label or a future one";
-  let res = reset_to_gen (is_label_n n) in
+  reset_to_gen (is_label_n n);
   (* forget state numbers after n only if reset succeeded *)
-  set_command_label (n-1);
-  res
+  reset_command_label n
 
-let rec back_stk n stk =
-  match stk with
-      (sp,Leaf o)::tail when object_tag o = "DOT" ->
-        if n=0 then sp else back_stk (n-1) tail
-    | _::tail -> back_stk n tail
-    | [] -> error "Reached begin of command history"
+(** Search the last label registered before defining [id] *)
 
-let back n =
-  reset_to (back_stk n !lib_stk);
-  set_command_label (current_command_label () - n - 1)
+let label_before_name (loc,id) =
+  let found = ref false in
+  let search = function
+    | (_,Leaf o) when !found && object_tag o = "DOT" -> true
+    | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+  in
+  match find_entry_p search with
+    | (_,Leaf o) -> outLabel o
+    | _ -> raise Not_found
 
 (* State and initialization. *)
 
@@ -684,29 +628,6 @@ let init () =
   path_prefix := initial_prefix;
   init_summaries()
 
-(* Initial state. *)
-
-let initial_state = ref None
-
-let declare_initial_state () =
-  let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
-  initial_state := Some name
-
-let reset_initial () =
-  match !initial_state with
-    | None ->
-        error "Resetting to the initial state is possible only interactively"
-    | Some sp ->
-  	begin match split_lib sp with
-	  | (_,[_,FrozenState fs as hd],before) ->
-	      lib_stk := hd::before;
-	      recalc_path_prefix ();
-			set_command_label 0;
-	      unfreeze_summaries fs
-	  | _ -> assert false
-	end
-
-
 (* Misc *)
 
 let mp_of_global ref =