- condition de garde (suite)

- commande Back


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index b2e73d1ce..f989ce988 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -36,7 +36,7 @@ and library_segment = library_entry list
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *) 
 
-let lib_stk = ref ([] : (section_path * node) list)
+let lib_stk = ref ([] : library_segment)
 
 let module_name = ref None
 let path_prefix = ref (default_module : dir_path)
@@ -232,6 +232,30 @@ let reset_name id =
   in
   reset_to sp
 
+let point_obj =
+  let (f,_) =
+    declare_object
+      ("DOT",
+       {cache_function = (fun _ -> ());
+        load_function = (fun _ -> ());
+        open_function = (fun _ -> ());
+        export_function = (fun _ -> None) }) in
+  f()
+
+let mark_end_of_command () =
+  match !lib_stk with
+      (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+    | _ -> add_anonymous_leaf point_obj
+
+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"
+
+let back n = reset_to (back_stk n !lib_stk)
+
 (* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
 let is_section_p sp =
   not (is_dirpath_prefix_of sp (module_sp ()))
diff --git a/library/lib.mli b/library/lib.mli
index f335d48ad..b86c08f72 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -37,7 +37,7 @@ val add_leaf : identifier -> obj -> section_path
 val add_absolutely_named_leaf : section_path -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 val add_frozen_state : unit -> unit
-
+val mark_end_of_command : unit -> unit
 
 (*s The function [contents_after] returns the current library segment, 
     starting from a given section path. If not given, the entire segment
@@ -67,7 +67,7 @@ val export_module : dir_path -> library_segment
 
 val reset_to : section_path -> unit
 val reset_name : identifier -> unit
-
+val back : int -> unit
 
 (*s We can get and set the state of the operations (used in [States]). *)