prise en compte de Load par coqdep

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

2 files changed, 36 insertions, 3 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 272724944b..a92c28220a 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -146,6 +146,15 @@ let traite_fichier_Coq f =
               	     with Not_found -> () 
 		   end)
 		sl
+	  | Load str -> 
+	      let str = Filename.basename str in
+	      if not (List.mem str !deja_vu_v) then begin
+	        deja_vu_v := str :: !deja_vu_v;
+                try
+                  let vdir = List.assoc str !vKnown in
+                  printf " %s.v" (file_name (str,vdir))
+                with Not_found -> ()
+       	      end
       done
     with Fin_fichier -> ();
       close_in chan
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 29e4b04a32..75352d6313 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -9,7 +9,8 @@
 (*i $Id$ i*)
   
 {
- 
+
+  open Filename 
   open Lexing
    
   type mL_token = Use_module of string
@@ -20,6 +21,7 @@
     | Require of spec * string
     | RequireString of spec * string
     | Declare of string list
+    | Load of string
 
   let mlAccu  = ref ([] : (string * string * string option) list) 
   and mliAccu = ref ([] : (string * string * string option) list) 
@@ -70,12 +72,16 @@ rule coq_action = parse
       { specif := false; opened_file lexbuf}
   | "Declare" space+ "ML" space+ "Module" space+
       { mllist := []; modules lexbuf}
+  | "Load" space+
+      { load_file lexbuf }
   | "\""
       { string lexbuf; coq_action lexbuf}
   | "(*"
       { comment_depth := 1; comment lexbuf; coq_action lexbuf }  
-  | eof { raise Fin_fichier} 
-  | _   { coq_action lexbuf }
+  | eof 
+      { raise Fin_fichier} 
+  | _   
+      { coq_action lexbuf }
 
 and caml_action = parse
   | [' ' '\010' '\013' '\009' '\012'] +
@@ -157,6 +163,24 @@ and string = parse
   | _
       { string lexbuf }
 
+and load_file = parse
+  | '"' [^ '"']* '"'
+      { let s = lexeme lexbuf in
+	let f = String.sub s 1 (String.length s - 2) in
+	skip_to_dot lexbuf;
+	Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
+  | coq_ident
+      { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
+  | eof	
+      { raise Fin_fichier }
+  | _
+      { load_file lexbuf }
+
+and skip_to_dot = parse
+  | '.' { () }
+  | eof { () }
+  | _   { skip_to_dot lexbuf }
+
 and opened_file = parse
   | "(*"  	{ comment_depth := 1; comment lexbuf; opened_file lexbuf }
   | space+