From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 toplevel/coqtop.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'toplevel/coqtop.ml')

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
 
-- 
cgit v1.2.3