diff options
| author | ppedrot | 2013-05-12 15:33:40 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-12 15:33:40 +0000 |
| commit | de26e97cf37cafd37b83377d2df062a6e82676e7 (patch) | |
| tree | 1f093c94b7cb8ab59f301b9c5ee7ca712aa9fa0f /parsing | |
| parent | 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 (diff) | |
Use the Hook module here and there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 5 | ||||
| -rw-r--r-- | parsing/lexer.mli | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index bf30d9d35f..81cfd3f1dc 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -288,8 +288,7 @@ let rec string in_comments bp len = parser | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string (* Hook for exporting comment into xml theory files *) -let xml_output_comment = ref (fun _ -> ()) -let set_xml_output_comment f = xml_output_comment := f +let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () (* Utilities for comments in beautify *) let comment_begin = ref None @@ -335,7 +334,7 @@ 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 - !xml_output_comment current_s; + 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 cef53a8710..8eef2f63c3 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -31,7 +31,7 @@ type com_state val com_state: unit -> com_state val restore_com_state: com_state -> unit -val set_xml_output_comment : (string -> unit) -> unit +val xml_output_comment : (string -> unit) Hook.t val terminal : string -> Tok.t |