aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
commit62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch)
treee4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /interp
parent97da8221e0097ed365f0a99e4960148424a59734 (diff)
Added checksums to glob files and warned about possibly missing
packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r--interp/dumpglob.ml19
-rw-r--r--interp/dumpglob.mli4
2 files changed, 20 insertions, 3 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 26f4d4e19..4a8756b88 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -31,8 +31,6 @@ let noglob () = glob_output := NoGlob
let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
-let multi_dump () = !glob_output = MultFiles
-
let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
@@ -40,6 +38,23 @@ let dump_into_file f = glob_output := File f; open_glob_file f
let dump_string s =
if dump () then Pervasives.output_string !glob_file s
+let start_dump_glob vfile =
+ match !glob_output with
+ | MultFiles ->
+ open_glob_file (Filename.chop_extension vfile ^ ".glob");
+ output_string !glob_file "DIGEST ";
+ output_string !glob_file (Digest.to_hex (Digest.file vfile));
+ output_char !glob_file '\n'
+ | File f ->
+ open_glob_file f;
+ output_string !glob_file "DIGEST NO\n"
+ | NoGlob | StdOut ->
+ ()
+
+let end_dump_glob () =
+ match !glob_output with
+ | MultFiles | File _ -> close_glob_file ()
+ | NoGlob | StdOut -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index c8f19ead0..b02cc9669 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -9,8 +9,10 @@
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
+val start_dump_glob : string -> unit
+val end_dump_glob : unit -> unit
+
val dump : unit -> bool
-val multi_dump : unit -> bool
val noglob : unit -> unit
val dump_to_stdout : unit -> unit