Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.

4 files changed, 14 insertions, 1 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5937fd5c7b..73ab77d08c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -546,6 +546,7 @@ let parse_args arglist =
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-verbose-compat-notations" -> verb_compat_ntn := true
     |"-where" -> print_where := true
+    |"-xml" -> Flags.xml_export := true
 
     (* Deprecated options *)
     |"-byte" -> warning "option -byte deprecated, call with .byte suffix"
@@ -561,7 +562,6 @@ let parse_args arglist =
     |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
     |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
     |"-quality" -> warning "Obsolete option \"-quality\"."
-    |"-xml" -> warning "Obsolete option \"-xml\"."
 
     (* Unknown option *)
     | s -> extras := s :: !extras
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 472503ced2..6ef5d01089 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -73,6 +73,9 @@ let print_usage_channel co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
+\n  -xml                   export XML files either to the hierarchy rooted in\
+\n                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
+\n                         stdout (if unset)\
 \n  -time                  display the time taken by each command\
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a0cd618e99..ada32ec3a2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -277,6 +277,10 @@ let checknav loc ast =
 
 let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
+(* XML output hooks *)
+let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
+let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
+
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
@@ -311,6 +315,7 @@ let compile verbosely f =
       Aux_file.start_aux_file_for long_f_dot_v;
       Dumpglob.start_dump_glob long_f_dot_v;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+      if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.join ();
@@ -320,6 +325,7 @@ let compile verbosely f =
       Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
+      if !Flags.xml_export then Hook.get f_xml_end_library ();
       Dumpglob.end_dump_glob ()
   | BuildVio ->
       let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index affc21713d..62e9f23904 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -23,6 +23,10 @@ val just_parsing : bool ref
 
 val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
 
+(** Set XML hooks *)
+val xml_start_library : (unit -> unit) Hook.t
+val xml_end_library   : (unit -> unit) Hook.t
+
 (** Load a vernac file, verbosely or not. Errors are annotated with file
    and location *)