Many changes in the Makefile infrastructure + a beginning of ocamlbuild

 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

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

1 files changed, 13 insertions, 16 deletions

diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 6d6a804da..3c7d09e1f 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -34,15 +34,18 @@
   let mllist = ref ([] : string list)
 
   let field_name s = String.sub s 1 (String.length s - 1)
+
 }
 
 let space = [' ' '\t' '\n' '\r']
 let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
 let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar = 
+let identchar =
   ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
 let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
+let caml_up_ident = uppercase identchar*
+let caml_low_ident = lowercase identchar*
 let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
@@ -66,13 +69,14 @@ rule coq_action = parse
       { coq_action lexbuf }
 
 and caml_action = parse
-  | [' ' '\010' '\013' '\009' '\012'] +
-      { caml_action lexbuf }
-  | "open" [' ' '\010' '\013' '\009' '\012']*
-        { caml_opened_file lexbuf }
-  | lowercase identchar*
+  | space +
       { caml_action lexbuf }
-  | uppercase identchar*
+  | "open" space* (caml_up_ident as id)
+        { Use_module (String.uncapitalize id) }
+  | "module" space+ caml_up_ident
+        { caml_action lexbuf }
+  | caml_low_ident { caml_action lexbuf }
+  | caml_up_ident
       { ml_module_name := Lexing.lexeme lexbuf;
         qual_id lexbuf }
   | ['0'-'9']+
@@ -213,18 +217,11 @@ and modules = parse
   | _   { (Declare (List.rev !mllist)) }   
 
 and qual_id = parse
-  | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) }
+  | '.' [^ '.' '(' '['] {
+      Use_module (String.uncapitalize !ml_module_name) }
   | eof { raise Fin_fichier }
   | _ { caml_action lexbuf }
 
-and caml_opened_file = parse
-  | uppercase identchar*
-      { let lex = (Lexing.lexeme lexbuf) in 
-        let str = String.sub lex 0 (String.length lex) in
-        (Use_module (String.uncapitalize str)) }
-  | eof {raise Fin_fichier }
-  | _ { caml_action lexbuf }
-
 and mllib_list = parse
   | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }