diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-26 21:55:21 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-26 21:55:21 +0000 |
commit | 2e43a5bd52cf2b83aa3624b27d0a5bef4d4b72ff (patch) | |
tree | 6c43ed258138801085ad8d8f6ff2fd435f0ba143 | |
parent | 72b8331c95e28605f7327f51e6c98920a9062fab (diff) |
Prise en compte du Require multiple
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tools/coqdep.ml | 31 | ||||
-rwxr-xr-x | tools/coqdep_lexer.mll | 38 |
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 } |