diff options
| author | herbelin | 2003-09-24 10:27:11 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-24 10:27:11 +0000 |
| commit | 79798540eba9424b14eccb3a6e6fd486cd40c3b2 (patch) | |
| tree | 5db343e1a46ef2bae6e3ea44706284822178a84b | |
| 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
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 9 |
2 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 992c45f445..1d8b4de638 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -61,7 +61,7 @@ let add_load_vernacular s = load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list let load_vernacular () = List.iter - (fun s -> Vernac.load_vernac false s) + (fun s -> with_option translate_file (Vernac.load_vernac false) s) (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 58cd8f53b1..e0f6b989de 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") |