diff options
| author | notin | 2008-07-21 14:29:13 +0000 |
|---|---|---|
| committer | notin | 2008-07-21 14:29:13 +0000 |
| commit | cb615fd741353dde4a562e1b4098c9e622b93f32 (patch) | |
| tree | f7d8de9cb89178e1ce961de40494c231eae9110d /interp | |
| parent | 71a52ff39091cda3e51d47a082bef610b016c2b8 (diff) | |
Suite commit 11236
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11240 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index b8121af866..ca817b776b 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -25,23 +25,26 @@ let dump_string s = Pervasives.output_string !glob_file s type glob_output_t = - | None + | NoGlob | StdOut | MultFiles | File of string -let glob_output = ref MultFiles +let glob_output = ref NoGlob -let dump () = !glob_output != None +let dump () = !glob_output != NoGlob -let noglob () = glob_output := None +let noglob () = glob_output := NoGlob -let dump_to_stdout () = glob_output := StdOut +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 + let previous_state = ref MultFiles let pause () = previous_state := !glob_output let continue () = glob_output := !previous_state |