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 | |
| parent | 0c566066f92728d9a848e1f60f52dd09c1a727f2 (diff) | |
| parent | 2def58217686b5083da38778a5ebffb451b1d4d6 (diff) | |
Merge PR #773: [flags] Remove XML output flag.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml4 | 6 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 3 |
2 files changed, 0 insertions, 9 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 diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 09c9d8ee4..77d652b18 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -19,9 +19,6 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit - -val xml_output_comment : (string -> unit) Hook.t - val terminal : string -> Tok.t (** The lexer of Coq: *) |