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

2 files changed, 8 insertions, 0 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c6d5f3b925..022f19fdbb 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 2b9bd37df7..2da3f3bfd9 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: *)