diff options
author | 2002-02-14 14:39:07 +0000 | |
---|---|---|
committer | 2002-02-14 14:39:07 +0000 | |
commit | 67f72c93f5f364591224a86c52727867e02a8f71 (patch) | |
tree | ecf630daf8346e77e6620233d8f3e6c18a0c9b3c /lib | |
parent | b239b208eb9a66037b0c629cf7ccb6e4b110636a (diff) |
option -dump-glob pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r-- | lib/options.ml | 21 | ||||
-rw-r--r-- | lib/options.mli | 7 |
2 files changed, 28 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml index 8d49d6b75..f1e40a89e 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -54,3 +54,24 @@ let print_hyps_limit () = !print_hyps_limit let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set + + +(* Dump of globalization (to be used by coqdoc) *) + +let dump = ref false +let dump_file = ref "" +let dump_into_file f = dump := true; dump_file := f + +let dump_buffer = Buffer.create 8192 + +let dump_string = Buffer.add_string dump_buffer + +let dump_it () = + if !dump then begin + let mode = [Open_wronly; Open_append; Open_creat] in + let c = open_out_gen mode 0o666 !dump_file in + output_string c (Buffer.contents dump_buffer); + close_out c + end + +let _ = at_exit dump_it diff --git a/lib/options.mli b/lib/options.mli index e8f7a2780..efc8617de 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -34,3 +34,10 @@ val print_hyps_limit : unit -> int option val add_unsafe : string -> unit val is_unsafe : string -> bool + +(* Dump of globalization (to be used by coqdoc) *) + +val dump : bool ref +val dump_into_file : string -> unit +val dump_string : string -> unit + |