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

22 files changed, 124 insertions, 26 deletions

diff --git a/Makefile.build b/Makefile.build
index 032f46508..48f448ce8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -587,9 +587,9 @@ pluginsbyte: $(PLUGINS)
 ###########################################################################
 
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
-	$(SHOW)'COQC -noinit $<'
+	$(SHOW)'COQC $(COQ_XML) -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
diff --git a/lib/flags.ml b/lib/flags.ml
index ab4ac03f8..bdae0adc9 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -83,6 +83,8 @@ let profile = false
 let print_emacs = ref false
 let coqtop_ui = ref false
 
+let xml_export = ref false
+
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 8e3713656..be2682cbd 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -44,6 +44,8 @@ val profile : bool
 val print_emacs : bool ref
 val coqtop_ui : bool ref
 
+val xml_export : bool ref
+
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
diff --git a/library/declare.ml b/library/declare.ml
index 994a6557a..8d86c4cf0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -32,6 +32,14 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
+(** XML output hooks *)
+
+let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
+let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
+let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
+
+let if_xml f x = if !Flags.xml_export then f x else ()
+
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -83,6 +91,7 @@ let declare_variable id obj =
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
   Heads.declare_head (EvalVarRef id);
+  if_xml (Hook.get f_xml_declare_variable) oname;
   oname
 
 
@@ -216,6 +225,7 @@ let declare_constant_common id cst =
       let id = Label.to_id (pi3 (Constant.repr3 c)) in
       ignore(add_leaf id o);
       update_tables c;
+      let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
       match role with
       | Safe_typing.Subproof -> ()
       | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
@@ -257,6 +267,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
     cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
+  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
 let declare_definition ?(internal=UserIndividualRequest)
@@ -365,8 +376,9 @@ let declare_projections mind =
 	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
-	  assert(eq_constant kn kn')) kns; true
-    | Some None | None -> false
+	  assert(eq_constant kn kn')) kns; true,true
+    | Some None -> true,false
+    | None -> false,false
 
 (* for initial declaration *)
 let declare_mind mie =
@@ -375,9 +387,10 @@ let declare_mind mie =
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
-  let isprim = declare_projections mind in
+  let isrecord,isprim = declare_projections mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
+  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
   oname, isprim
 
 (* Declaration messages *)
diff --git a/library/declare.mli b/library/declare.mli
index c6119a58a..60676ff43 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -71,6 +71,11 @@ val set_declare_scheme :
    the whole block and a boolean indicating if it is a primitive record. *)
 val declare_mind : mutual_inductive_entry -> object_name * bool
 
+(** Hooks for XML output *)
+val xml_declare_variable : (object_name -> unit) Hook.t
+val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
+val xml_declare_inductive : (bool * object_name -> unit) Hook.t
+
 (** Declaration messages *)
 
 val definition_message : Id.t -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7f607a51c..0162de10c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -557,6 +557,17 @@ let openmodtype_info =
   Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"
 
 
+(** XML output hooks *)
+
+let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore ()
+let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore ()
+let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore ()
+let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore ()
+let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore ()
+let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore ()
+
+let if_xml f x = if !Flags.xml_export then f x else ()
+
 (** {6 Modules : start, end, declare} *)
 
 module RawModOps = struct
@@ -578,7 +589,9 @@ let start_module interp_modast export id args res fs =
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  Lib.add_frozen_state (); mp
+  Lib.add_frozen_state ();
+  if_xml (Hook.get f_xml_start_module) mp;
+  mp
 
 let end_module () =
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
@@ -617,6 +630,7 @@ let end_module () =
   assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
   Lib.add_frozen_state () (* to prevent recaching *);
+  if_xml (Hook.get f_xml_end_module) mp;
   mp
 
 let declare_module interp_modast id args res mexpr_o fs =
@@ -666,6 +680,7 @@ let declare_module interp_modast id args res mexpr_o fs =
 
   let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
   ignore (Lib.add_leaf id (in_module sobjs));
+  if_xml (Hook.get f_xml_declare_module) mp;
   mp
 
 end
@@ -682,7 +697,9 @@ let start_modtype interp_modast id args mtys fs =
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  Lib.add_frozen_state (); mp
+  Lib.add_frozen_state ();
+  if_xml (Hook.get f_xml_start_module_type) mp;
+  mp
 
 let end_modtype () =
   let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
@@ -699,6 +716,7 @@ let end_modtype () =
   assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
   Lib.add_frozen_state ()(* to prevent recaching *);
+  if_xml (Hook.get f_xml_end_module_type) mp;
   mp
 
 let declare_modtype interp_modast id args mtys (mty,ann) fs =
@@ -729,6 +747,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   check_subtypes_mt mp sub_mty_l;
 
   ignore (Lib.add_leaf id (in_modtype sobjs));
+  if_xml (Hook.get f_xml_declare_module_type) mp;
   mp
 
 end
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 319d168d0..8b9f70b35 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -63,6 +63,13 @@ val start_modtype :
 
 val end_modtype : unit -> module_path
 
+(** Hooks for XML output *)
+val xml_declare_module : (module_path -> unit) Hook.t
+val xml_start_module : (module_path -> unit) Hook.t
+val xml_end_module : (module_path -> unit) Hook.t
+val xml_declare_module_type : (module_path -> unit) Hook.t
+val xml_start_module_type : (module_path -> unit) Hook.t
+val xml_end_module_type : (module_path -> unit) Hook.t
 
 (** {6 Libraries i.e. modules on disk } *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 297441e6e..42cea4de8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -497,6 +497,10 @@ let full_section_segment_of_constant con =
 (*************)
 (* Sections. *)
 
+(* XML output hooks *)
+let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
+let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
+
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
   let dir = add_dirpath_suffix olddir id in
@@ -508,6 +512,7 @@ let open_section id =
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
+  if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
 
@@ -536,6 +541,7 @@ let close_section () =
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
+  if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
diff --git a/library/lib.mli b/library/lib.mli
index bb8831759..398149a50 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -157,6 +157,10 @@ val unfreeze : frozen -> unit
 
 val init : unit -> unit
 
+(** XML output hooks *)
+val xml_open_section : (Names.Id.t -> unit) Hook.t
+val xml_close_section : (Names.Id.t -> unit) Hook.t
+
 (** {6 Section management for discharge } *)
 type variable_info = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
diff --git a/library/library.ml b/library/library.ml
index 024ac9e6f..365d119dd 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -555,6 +555,8 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
+let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
+
 let require_library_from_dirpath modrefl export =
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
@@ -568,6 +570,7 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
+    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index d5e610dd6..fb0ce4795 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -67,6 +67,9 @@ val library_full_filename : DirPath.t -> string
   (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
+(** {6 Hook for the xml exportation of libraries } *)
+val xml_require : (DirPath.t -> unit) Hook.t
+
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound
diff --git a/man/coqide.1 b/man/coqide.1
index 6a3e67ad5..f82bf2ad4 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -123,6 +123,12 @@ Set sort Set impredicative.
 .TP
 .B \-dont\-load\-proofs
 Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
 
 
 .SH SEE ALSO
diff --git a/man/coqtop.1 b/man/coqtop.1
index 62d17aa67..feee7fd8b 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -153,6 +153,12 @@ set sort Set impredicative
 .B \-dont\-load\-proofs
 don't load opaque proofs in memory
 
+.TP
+.B \-xml
+export XML files either to the hierarchy rooted in
+the directory $COQ_XML_LIBRARY_ROOT (if set) or to
+stdout (if unset)
+
 .SH SEE ALSO
 
 .BR coqc (1),
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c6d5f3b92..022f19fdb 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -298,6 +298,9 @@ let rec string in_comments bp len = parser
   | [< 'c; s >] -> string in_comments bp (store len c) s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
 
+(* Hook for exporting comment into xml theory files *)
+let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
+
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = match !comment_begin with
@@ -340,6 +343,9 @@ let null_comment s =
 
 let comment_stop ep =
   let current_s = Buffer.contents current in
+  if !Flags.xml_export && Buffer.length current > 0 &&
+    (!between_com || not(null_comment current_s)) then
+      Hook.get f_xml_output_comment current_s;
   (if Flags.do_beautify() && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
     let bp = match !comment_begin with
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 2b9bd37df..2da3f3bfd 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -29,6 +29,8 @@ type com_state
 val com_state: unit -> com_state
 val restore_com_state: com_state -> unit
 
+val xml_output_comment : (string -> unit) Hook.t
+
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/plugins/xml/README b/plugins/xml/README
index e3bcdaf05..312818992 100644
--- a/plugins/xml/README
+++ b/plugins/xml/README
@@ -1,15 +1,4 @@
-The xml export plugin for Coq has been discontinued for lack of users:
-it was most certainly broken while imposing a non-negligible cost on
-Coq development. Its purpose was to give export Coq's kernel objects
-in xml form for treatment by external tools.
-
-If you are looking for such a tool, you may want to look at commit
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 responsible for the deletion
-of this plugin (for instance, git checkout
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9^ including the "^", will lead
-you to the last commit before the xml plugin was deleted).
-
-Bear in mind, however, that the plugin was not working properly at the
-time. You may want instead to write to the original author of the
-plugin, Claudio Sacerdoti-Coen at sacerdot@cs.unibo.it. He has a
-stable version of the plugin for an old version of Coq.
+The xml export plugin for Coq has been removed from the sources.
+A backward compatible plug-in will be provided as a third-party plugin.
+For more informations, contact
+Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>.
diff --git a/stm/stm.ml b/stm/stm.ml
index 168d8bf08..5a34e8111 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -53,6 +53,9 @@ let execution_error, execution_error_hook = Hook.make
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
+let tactic_being_run, tactic_being_run_hook = Hook.make
+ ~default:(fun _ -> ()) ()
+
 include Hook
 
 (* enables:  Hooks.(call foo args) *)
@@ -1800,16 +1803,21 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
             reach ~cache:`Shallow view.next;
+            Hooks.(call tactic_being_run true); 
             Partac.vernac_interp
-              cancel !Flags.async_proofs_n_tacworkers view.next id x
+              cancel !Flags.async_proofs_n_tacworkers view.next id x;
+            Hooks.(call tactic_being_run false)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
             reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
-      | `Cmd { cast = x; ceff = eff } -> (fun () ->
-            reach view.next; vernac_interp id x;
+      | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
+            reach view.next;
+            if ctac then Hooks.(call tactic_being_run true); 
+            vernac_interp id x;
+            if ctac then Hooks.(call tactic_being_run false); 
 	    if eff then update_global_env ()), cache, true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
@@ -2590,4 +2598,5 @@ let interp_hook = Hooks.interp_hook
 let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
 let get_fix_exn () = !State.fix_exn_ref
+let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 0c05c93d4..ad89eb71f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -107,6 +107,9 @@ val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
+(* called with true before and with false after a tactic explicitly
+ * in the document is run *)
+val tactic_being_run_hook : (bool -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5937fd5c7..73ab77d08 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 472503ced..6ef5d0108 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 a0cd618e9..ada32ec3a 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 affc21713..62e9f2390 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 *)