Ajout entree pour exporter les debuts et fins de compilation en mode -xml

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

2 files changed, 14 insertions, 14 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f72c533e1e..7768fa95b3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -264,6 +264,13 @@ let raw_do_vernac po =
   vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
   Lib.mark_end_of_command()
 
+(* XML output hooks *)
+let xml_start_library = ref (fun _ -> ())
+let xml_end_library = ref (fun _ -> ())
+
+let set_xml_start_library f = xml_start_library := f
+let set_xml_end_library f = xml_end_library := f
+
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_translate :=
@@ -277,23 +284,12 @@ let load_vernac verb file =
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-(*
-    let s = Filename.basename f in
-    let m = Names.id_of_string s in
-    let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
-    let ldir0 = Library.find_logical_path (Filename.dirname longf) in
-    let ldir = Libnames.extend_dirpath ldir0 m in
-    Termops.set_module ldir; (* Just for universe naming *)
-    Lib.start_module ldir;
-    if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
-    let _ = load_vernac verbosely longf in
-    let mid = Lib.end_module m in
-    assert (mid = ldir);
-    Library.save_module_to ldir (longf^"o")
-*)
   let ldir,long_f_dot_v = Library.start_library f in
   if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+  if !Options.xml_export then !xml_start_library ();
   let _ = load_vernac verbosely long_f_dot_v in
   if Pfedit.get_all_proof_names () <> [] then
     (message "Error: There are pending proofs"; exit 1);
+  if !Options.xml_export then !xml_end_library ();
   Library.save_library_to ldir (long_f_dot_v ^ "o")
+
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 37279a2d52..c0f8f44f59 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -25,6 +25,10 @@ exception End_of_input
 val just_parsing : bool ref
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
+(* Set XML hooks *)
+val set_xml_start_library : (unit -> unit) -> unit
+val set_xml_end_library   : (unit -> unit) -> unit
+
 (* Load a vernac file, verbosely or not. Errors are annotated with file
    and location *)