diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /toplevel/coqtop.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e6d2deec..f8c57ad2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 11062 2008-06-06 14:19:50Z notin $ *) +(* $Id: coqtop.ml 11209 2008-07-05 10:17:49Z herbelin $ *) open Pp open Util @@ -72,10 +72,12 @@ let check_coq_overwriting p = if string_of_id (list_last (repr_dirpath p)) = "Coq" then error "The \"Coq\" logical root directory is reserved for the Coq library" -let set_include d p = push_include (d,p) -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 set_default_include d = push_include (d,Nameops.default_root_prefix) +let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix) +let set_include d p = + let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) +let set_rec_include d p = + let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -187,15 +189,22 @@ let parse_args is_ide = | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: [] -> usage () | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem + | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem + | "-R" :: d :: "-as" :: [] -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem | "-top" :: [] -> usage () + | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem + | "-exclude-dir" :: [] -> usage () + | "-notop" :: rem -> unset_toplevel_name (); parse rem | "-q" :: rem -> no_load_rc (); parse rem |