Prise en compte du Require multiple

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

2 files changed, 39 insertions, 30 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2b5d192db..f8ee39a58 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -162,8 +162,12 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require (_, s) ->
-		(try loop (List.assoc s !vKnown) with Not_found -> ())
+	    | Require (_, sl) ->
+		List.iter 
+		  (fun s -> 
+		    try loop (List.assoc s !vKnown) 
+		    with Not_found -> ())
+		sl
 	    | RequireString (_, s) -> loop s
 	    | _ -> ()
 	done
@@ -184,17 +188,18 @@ let traite_fichier_Coq verbose f =
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require (spec,str) ->
-	      if not (List.mem str !deja_vu_v) then begin
-	        addQueue deja_vu_v str;
-                try
-                  let file_str = safe_assoc verbose f str in
-                  printf " %s%s" (canonize file_str)
-                    (if spec then !suffixe_spec else !suffixe)
-                with Not_found -> 
-		  if verbose && not (List.mem_assoc str !coqlibKnown) then
-                    warning_module_notfound f str
-       	      end
+	  | Require (spec,strl) ->
+	      List.iter (fun str ->
+		if not (List.mem str !deja_vu_v) then begin
+	          addQueue deja_vu_v str;
+                  try
+                    let file_str = safe_assoc verbose f str in
+                    printf " %s%s" (canonize file_str)
+                      (if spec then !suffixe_spec else !suffixe)
+                  with Not_found -> 
+		    if verbose && not (List.mem_assoc str !coqlibKnown) then
+                      warning_module_notfound f str
+       		end) strl
 	  | RequireString (spec,s) -> 
 	      let str = Filename.basename s in
 	      if not (List.mem [str] !deja_vu_v) then begin
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 0d287e318..ffb35c528 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -18,7 +18,7 @@
   type spec = bool
 		
   type coq_token = 
-    | Require of spec * string list
+    | Require of spec * string list list
     | RequireString of spec * string
     | Declare of string list
     | Load of string
@@ -27,7 +27,8 @@
  
   exception Fin_fichier
     
-  let module_name = ref []
+  let module_current_name = ref []
+  let module_names = ref []
   let ml_module_name = ref ""
 		      
   let specif = ref false
@@ -48,13 +49,11 @@ let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { specif := false; opened_file lexbuf }
+      { specif := false; module_names := []; opened_file lexbuf }
   | "Require" space+ "Export" space+
-      { specif := false; opened_file lexbuf}
-  | "Require" space+ "Syntax" space+
-      { specif := false; opened_file lexbuf}
+      { specif := false; module_names := []; opened_file lexbuf}
   | "Require" space+ "Import" space+
-      { specif := false; opened_file lexbuf}
+      { specif := false; module_names := []; opened_file lexbuf}
   | "Declare" space+ "ML" space+ "Module" space+
       { mllist := []; modules lexbuf}
   | "Load" space+
@@ -175,7 +174,7 @@ and opened_file = parse
   | "Specification"
                 { specif := true; opened_file lexbuf }
   | coq_ident
-       	       	{ module_name := [Lexing.lexeme lexbuf];
+       	       	{ module_current_name := [Lexing.lexeme lexbuf];
                   opened_file_fields lexbuf }
 
   | '"' [^'"']* '"'   { (*'"'*)
@@ -186,23 +185,28 @@ and opened_file = parse
                             Filename.chop_suffix str ".v"
                           else str in
 			RequireString (!specif, str) }
-  | eof		      { raise Fin_fichier }
-  | _		      { opened_file lexbuf }
+  | eof         { raise Fin_fichier }
+  | _           { opened_file lexbuf }
 
 and opened_file_fields = parse
   | "(*" (* "*)" *)
                 { comment_depth := 1; comment lexbuf;
                   opened_file_fields lexbuf }
   | space+
-      	       	{ opened_file_fields lexbuf }
+                { opened_file_fields lexbuf }
   | coq_field
-       	       	{ module_name :=
-                    field_name (Lexing.lexeme lexbuf) :: !module_name;
+                { module_current_name :=
+                    field_name (Lexing.lexeme lexbuf) :: !module_current_name;
                   opened_file_fields lexbuf }
-  | dot               { Require (!specif, List.rev !module_name) }
-  | eof		      { raise Fin_fichier }
-  | _		      { opened_file_fields lexbuf }
-
+  | coq_ident   { module_names := 
+                    List.rev !module_current_name :: !module_names;
+                  module_current_name := [Lexing.lexeme lexbuf];
+                  opened_file_fields lexbuf }
+  | dot         { module_names :=
+                    List.rev !module_current_name :: !module_names;
+                  Require (!specif, List.rev !module_names) }
+  | eof         { raise Fin_fichier }
+  | _           { opened_file_fields lexbuf }
 
 and modules = parse
   | space+              { modules lexbuf }