Ajout mémorisation numéro commande courante + reset vers ce numéro pour mode emacs

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

2 files changed, 21 insertions, 10 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 980fd7e4c..d6092ed4c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -493,15 +493,25 @@ let reset_mod (loc,id) =
   recache_context after
 
 
-let point_obj =
-  let (f,_) = declare_object {(default_object "DOT") with
-				classify_function = (fun _ -> Dispose)} in
-    f()
-
-let mark_end_of_command () =
-  match !lib_stk with
-      (_,Leaf o)::_ when object_tag o = "DOT" -> ()
-    | _ -> add_anonymous_leaf point_obj
+let (inLabel,outLabel) =
+  declare_object {(default_object "DOT") with
+				classify_function = (fun _ -> Dispose)}
+
+let mark_end_of_command, current_command_label =
+  let n = ref 0 in
+  (fun () ->
+    match !lib_stk with
+        (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+      | _ -> incr n; add_anonymous_leaf (inLabel !n)),
+  (fun () -> !n)
+
+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 reset_label n = reset_to (reset_label_stk n !lib_stk)
 
 let rec back_stk n stk =
   match stk with
diff --git a/library/lib.mli b/library/lib.mli
index c43155816..fa8a34344 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -66,7 +66,8 @@ val add_leaves : identifier -> obj list -> object_name
 
 val add_frozen_state : unit -> unit
 val mark_end_of_command : unit -> unit
-
+val current_command_label : unit -> int
+val reset_label : int -> unit
 
 (*s The function [contents_after] returns the current library segment, 
   starting from a given section path. If not given, the entire segment