diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:34:17 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:34:17 +0200 |
| commit | 75d70664156bf1715b4eb9933a684a344f43467d (patch) | |
| tree | 0f98f6fb7b1d39e8aae86c45ba7b2e36b3a91f53 /parsing/cLexer.ml4 | |
| parent | 0c566066f92728d9a848e1f60f52dd09c1a727f2 (diff) | |
| parent | 2def58217686b5083da38778a5ebffb451b1d4d6 (diff) | |
Merge PR #773: [flags] Remove XML output flag.
Diffstat (limited to 'parsing/cLexer.ml4')
| -rw-r--r-- | parsing/cLexer.ml4 | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 5fcbb43b6..636027f9b 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -368,9 +368,6 @@ let rec string loc ~comm_level bp len = parser let loc = set_loc_pos loc bp ep in err loc Unterminated_string -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - (* To associate locations to a file name *) let current_file = ref None @@ -432,9 +429,6 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current_comment in - if !Flags.xml_export && Buffer.length current_comment > 0 && - (!between_commands || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; (if !Flags.beautify && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with |