diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-24 10:27:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-24 10:27:11 +0000 |
| commit | 79798540eba9424b14eccb3a6e6fd486cd40c3b2 (patch) | |
| tree | 5db343e1a46ef2bae6e3ea44706284822178a84b /toplevel/vernac.ml | |
| parent | 5b060b7e8496b125ae46c8a0023d64c655da9557 (diff) | |
Traduction aussi si -translate et -load-vernac-source
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4471 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 58cd8f53b..e0f6b989d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -218,9 +218,13 @@ let raw_do_vernac po = (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = + chan_translate := + if Options.do_translate () then open_out (file^"8") else stdout; try - read_vernac_file verb file + read_vernac_file verb file; + if Options.do_translate () then close_out !chan_translate; with e -> + if Options.do_translate () then close_out !chan_translate; raise_with_file file e (* Compile a vernac file (f is assumed without .v suffix) *) @@ -241,10 +245,7 @@ let compile verbosely f = *) let ldir,long_f_dot_v = Library.start_library f in if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - chan_translate := - if Options.do_translate () then open_out (f^".v8") else stdout; let _ = load_vernac verbosely long_f_dot_v in - if Options.do_translate () then close_out !chan_translate; if Pfedit.get_all_proof_names () <> [] then (message "Error: There are pending proofs"; exit 1); Library.save_library_to ldir (long_f_dot_v ^ "o") |