diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-15 13:50:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-15 13:50:04 +0000 |
| commit | 8e83f994d6a4c50857ee25739108eaedc49078da (patch) | |
| tree | 720714b0ba1a212e7012b7d887da2d6472ec728a /toplevel | |
| parent | cf638246e73e6b9c0174457a532104be98573f13 (diff) | |
Ajout load-vernac-source-verbose
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f339f8d68..72ac4f086 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -73,16 +73,16 @@ let set_rec_include d p = check_coq_overwriting p; push_rec_include (d,p) let set_default_include d = set_include d Nameops.default_root_prefix let set_default_rec_include d = set_rec_include d Nameops.default_root_prefix -let load_vernacular_list = ref ([] : string list) -let add_load_vernacular s = - load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list +let load_vernacular_list = ref ([] : (string * bool) list) +let add_load_vernacular verb s = + load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list let load_vernacular () = List.iter - (fun s -> + (fun (s,b) -> if Options.do_translate () then - with_option translate_file (Vernac.load_vernac false) s + with_option translate_file (Vernac.load_vernac b) s else - Vernac.load_vernac false s) + Vernac.load_vernac b s) (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) @@ -192,9 +192,13 @@ let parse_args is_ide = | "-load-ml-source" :: [] -> usage () | ("-load-vernac-source"|"-l") :: f :: rem -> - add_load_vernacular f; parse rem + add_load_vernacular false f; parse rem | ("-load-vernac-source"|"-l") :: [] -> usage () + | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> + add_load_vernacular true f; parse rem + | ("-load-vernac-source-verbose"|"-lv") :: [] -> usage () + | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () |