diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-31 14:44:50 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-31 14:44:50 +0000 |
commit | 8594c30c6d492aea98f99947feb9ed9b325ecc19 (patch) | |
tree | 2cf90eb1c6592a4c8842db0290f3e798a6a59b94 /tools/coqdep_lexer.mll | |
parent | 08a35669ea650a408310154dc194bbbd400814a5 (diff) |
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
Diffstat (limited to 'tools/coqdep_lexer.mll')
-rwxr-xr-x | tools/coqdep_lexer.mll | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 29e4b04a3..75352d631 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+ |