From de26e97cf37cafd37b83377d2df062a6e82676e7 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 12 May 2013 15:33:40 +0000
Subject: 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
---
 parsing/lexer.ml4 | 5 ++---
 parsing/lexer.mli | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'parsing')

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
 
-- 
cgit v1.2.3