From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 22:12:02 +0200
Subject: [flags] Remove XML output flag.

This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.

It is also not included in the API, so it should either be included in
it or this PR be applied.
---
 toplevel/coqtop.ml  | 1 -
 toplevel/usage.ml   | 3 ---
 toplevel/vernac.ml  | 6 ------
 toplevel/vernac.mli | 4 ----
 4 files changed, 14 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8fe27b3b97..ba6d4b05b3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -585,7 +585,6 @@ let parse_args arglist =
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ())
     |"-where" -> print_where := true
-    |"-xml" -> Flags.xml_export := true
 
     (* Unknown option *)
     | s -> extras := s :: !extras
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 962bb4302b..d596e36f34 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -78,9 +78,6 @@ 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  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index fe853c093d..bfab447706 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -243,10 +243,6 @@ let process_expr sid loc_ast =
   checknav_deep loc_ast;
   interp_vernac sid 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 ()
-
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
          (fun (f,ext) ->
@@ -308,7 +304,6 @@ let compile verbosely f =
         ~v_file:long_f_dot_v);
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       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 (Stm.get_current_state ()) long_f_dot_v in
       Stm.join ();
@@ -318,7 +313,6 @@ let compile verbosely f =
       Aux_file.record_in_aux_at "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 77c4f44e12..bccf560e16 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -21,7 +21,3 @@ val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
 val compile : bool -> string -> unit
-
-(** Set XML hooks *)
-val xml_start_library : (unit -> unit) Hook.t
-val xml_end_library   : (unit -> unit) Hook.t
-- 
cgit v1.2.3