diff options
Diffstat (limited to 'parsing/lexer.ml4')
| -rw-r--r-- | parsing/lexer.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
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 |