Plusieurs arguments autorisés pour Require et Read Module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 71 insertions, 47 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 671338002..f68628eab 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -58,14 +58,21 @@ let ctf_FileErrorMessage reqid pps =
 (*In the code for CoqV6.2, the require_module call is encapsulated in
   a function "without_mes_ambig".  Here I have supposed that this
   function has no effect on parsing *)
-let try_require_module import specif name fname =
+let try_require_module import specif names =
  try Library.require_module 
    (if specif = "UNSPECIFIED" then None
     else Some (specif = "SPECIFICATION"))
-   (Nametab.make_short_qualid (Names.id_of_string name))
-   fname (import = "IMPORT")
+   (List.map (fun name -> Nametab.make_short_qualid (Names.id_of_string name))
+      names)
+   (import = "IMPORT")
  with
-   | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
+   | e -> msgnl (str "Reinterning of " ++ prlist str names ++ str " failed");;
+
+let try_require_module_from_file import specif name fname =
+ try Library.require_module_from_file (if specif = "UNSPECIFIED" then None
+  else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
+ with
+ | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
 
 let execute_when_necessary ast =
  (match ast with
@@ -74,13 +81,16 @@ let execute_when_necessary ast =
   | Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
   | Node (_, "Require",
             ((Str (_, import)) ::
-              ((Str (_, specif)) :: ((Nvar (_, mname)) :: [])))) ->
-   try_require_module import specif mname None
+              ((Str (_, specif)) :: l))) ->
+   let mnames = List.map (function
+     | (Nvar (_, m)) -> m
+     | _ -> error "parse_string_action : bad require expression") l in
+   try_require_module import specif mnames
   | Node (_, "RequireFrom",
             ((Str (_, import)) ::
               ((Str (_, specif)) ::
                 ((Nvar (_, mname)) :: ((Str (_, file_name)) :: []))))) ->
-   try_require_module import specif mname (Some file_name)
+   try_require_module_from_file import specif mname file_name
   | _ -> ()); ast;;
 
 let parse_to_dot =
@@ -371,8 +381,7 @@ let load_syntax_action reqid module_name =
       (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
       read_module qid;
       msg (str "opening... ");
-      let fullname = Nametab.locate_loaded_library qid in 
-      import_module fullname; 
+      import_module false qid; 
       msgnl (str "done" ++ fnl ());
       ())
  with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index caae9a1e4..0c2a61896 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -429,10 +429,11 @@ GEXTEND Gram
             <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
                       ($STR $mname) ($STR $fname))>>
 *)
-      | IDENT "Read"; IDENT "Module"; qid = qualidarg ->
-          <:ast< (ReadModule $qid) >>
+      | IDENT "Read"; IDENT "Module"; qidl = LIST1 qualidarg ->
+          <:ast< (ReadModule ($LIST $qidl)) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
-        qid = qualidarg -> <:ast< (Require $import $specif $qid) >>
+        qidl = LIST1 qualidarg ->
+          <:ast< (Require $import $specif ($LIST $qidl)) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
         qid = qualidarg; filename = stringarg ->
           <:ast< (RequireFrom $import $specif $qid $filename) >>
@@ -442,8 +443,10 @@ GEXTEND Gram
 	  <:ast< (WriteModule $id $s) >>
       | IDENT "Declare"; IDENT "ML"; IDENT "Module";
         l = ne_stringarg_list -> <:ast< (DeclareMLModule ($LIST $l)) >>
-      | IDENT "Import"; qid = qualidarg -> <:ast< (ImportModule $qid) >>
-
+      | IDENT "Import"; qidl = ne_qualidarg_list ->
+          <:ast< (ImportModule ($LIST $qidl)) >>
+      | IDENT "Export"; qidl = ne_qualidarg_list ->
+          <:ast< (ExportModule ($LIST $qidl)) >>
   ] 
 ]
   ;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3b98ce2f4..48c889474 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -70,7 +70,7 @@ let require () =
   List.iter
     (fun s -> 
       let qid = Nametab.make_short_qualid (id_of_string (Filename.basename s)) in
-      Library.require_module None qid  (Some s) false)
+      Library.require_module_from_file None qid s false)
     (List.rev !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b603b28e3..a72302458 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -348,23 +348,33 @@ let _ =
 
 let _ =
   add "ReadModule"
-    (function 
-       | [VARG_QUALID qid] ->
-	   fun () -> without_mes_ambig Library.read_module qid
-       | _ -> bad_vernac_args "ReadModule")
+    (function l ->
+       let l =
+         List.map
+           (function
+              | VARG_QUALID qid -> qid
+              | _ -> bad_vernac_args "ReadModule") l in
+       fun () -> List.iter Library.read_module l)
 
 let _ =
   add "ImportModule"
-    (function 
-       | [VARG_QUALID qid] ->
-	   fun () ->
-	     let fullname =
-               try Nametab.locate_loaded_library qid
-               with Not_found -> 
-                 error ((Nametab.string_of_qualid qid)^" not loaded")
-             in
-	     without_mes_ambig Library.import_module fullname
-       | _ -> bad_vernac_args "ImportModule")
+    (function l ->
+       let l =
+         List.map
+           (function
+              | VARG_QUALID qid -> qid
+              | _ -> bad_vernac_args "ImportModule") l in 
+       fun () -> List.iter (Library.import_module false) l)
+
+let _ =
+  add "ExportModule"
+    (function l ->
+       let l =
+         List.map
+           (function
+              | VARG_QUALID qid -> qid
+              | _ -> bad_vernac_args "ExportModule") l in
+       fun () -> List.iter (Library.import_module true) l)
 
 let _ =
   add "PrintModules"
@@ -1260,16 +1270,19 @@ let _ =
 let _ =
   add "Require"
     (function 
-       | [VARG_STRING import; VARG_STRING specif; VARG_QUALID qid] ->
-	   fun () -> 
-	     without_mes_ambig 
-	       (Library.require_module 
-      		  (if specif="UNSPECIFIED" then 
-		     None 
-		   else 
-		     Some (specif="SPECIFICATION"))
-		  qid None)
-      	       (import="EXPORT") 
+       | VARG_STRING import :: VARG_STRING specif :: l ->
+           let l =
+             List.map
+               (function
+                  | VARG_QUALID qid -> qid
+                  | _ -> bad_vernac_args "Require") l in
+           let spec =
+             if specif="UNSPECIFIED" then 
+	       None 
+	     else 
+	       Some (specif="SPECIFICATION") in
+           let export = (import="EXPORT") in
+	   fun () -> Library.require_module spec l export
        | _ -> bad_vernac_args "Require")
 
 let _ =
@@ -1278,14 +1291,13 @@ let _ =
        | [VARG_STRING import; VARG_STRING specif;
       	  VARG_QUALID qid; VARG_STRING filename] ->
 	   (fun () -> 
-	      without_mes_ambig 
-		(Library.require_module 
-      		   (if specif="UNSPECIFIED" then 
-		      None 
-		    else 
-		      Some (specif="SPECIFICATION"))
-		   qid (Some filename))
-		(import="EXPORT"))
+	      Library.require_module_from_file
+      		(if specif="UNSPECIFIED" then 
+		   None 
+		 else 
+		   Some (specif="SPECIFICATION"))
+		qid filename
+	        (import="EXPORT"))
        | _ -> bad_vernac_args "RequireFrom")
 
 let _ =