modifs mineures

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

1 files changed, 40 insertions, 17 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d47aeb014b..c7ef3f3540 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -66,13 +66,13 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
   exit 1
 
 let standard sds =
-  print "byte::\n";
+  print "byte:\n";
   print "\t$(MAKE) all \"OPT=\"\n\n";
-  print "opt::\n";
+  print "opt:\n";
   if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
   print "\t$(MAKE) all \"OPT="; print !opt ; print "\"\n\n";
   if !some_file then print "include .depend\n\n";
-  print "depend::\n";
+  print "depend:\n";
   if !some_file then begin
     print "\trm .depend\n";
     print "\t$(COQDEP) -i $(LIBS) *.v *.ml *.mli >.depend\n";
@@ -82,7 +82,7 @@ let standard sds =
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
     sds;
   print "\n";
-  print "install::\n";
+  print "install:\n";
   print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n";
   if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n";
   if !some_mlfile then print "\tcp -f *.cmo $(TARGETDIR)\n";
@@ -90,17 +90,17 @@ let standard sds =
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
     sds;
   print "\n";
-  print "Makefile::\n";
+  print "Makefile: Make\n";
   print "\tmv -f Makefile Makefile.bak\n";
-  print "\tcoq_makefile -f Make -o Makefile\n";
+  print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n";
   print "\n";
-  print "clean::\n";
+  print "clean:\n";
   print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~\n";
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n")
     sds;
   print "\n";
-  print "archclean::\n";
+  print "archclean:\n";
   print "\trm -f *.cmx *.o\n";
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
@@ -207,7 +207,7 @@ let subdirs l =
     | Subdir x :: r -> x::(subdirs_aux r)
     | _ :: r -> subdirs_aux r
   and pr_subdir s =
-    print s ; print "::\n\tcd " ; print s ; print " ; $(MAKE) all\n\n"
+    print s ; print ":\n\tcd " ; print s ; print " ; $(MAKE) all\n\n"
   in
   let sds = subdirs_aux l in
   if sds <> [] then section "Subdirectories.";
@@ -246,20 +246,20 @@ let all_target l =
     | [] -> []
   in
   section "Definition of the \"all\" target.";
-  print "all:: "; print_list "\\\n  " (fnames l) ;
+  print "all: "; print_list "\\\n  " (fnames l) ;
   print "\n\n" ;
   if !some_vfile then begin
-    print "spec:: "; print_list "\\\n  " (vifiles l) ;
+    print "spec: "; print_list "\\\n  " (vifiles l) ;
     print "\n\n";
-    print "gallina:: "; print_list "\\\n  " (gfiles l) ;
+    print "gallina: "; print_list "\\\n  " (gfiles l) ;
     print "\n\n";
-    print "html:: "; print_list "\\\n  " (hfiles l) ;
+    print "html: "; print_list "\\\n  " (hfiles l) ;
     print "\n\n";
-    print "tex:: "; print_list "\\\n  " (tfiles l) ;
+    print "tex: "; print_list "\\\n  " (tfiles l) ;
     print "\n\n";
-    print "gallinatex:: "; print_list "\\\n  " (gtfiles l) ;
+    print "gallinatex: "; print_list "\\\n  " (gtfiles l) ;
     print "\n\n";
-    print "gallinahtml:: "; print_list "\\\n  " (ghfiles l) ;
+    print "gallinahtml: "; print_list "\\\n  " (ghfiles l) ;
     print "\n\n";
   end
 
@@ -345,12 +345,34 @@ let warning () =
   print "# Edit at your own risks !\n";
   print "#\n# END OF WARNING\n\n"
 
+let print_list l = List.iter (fun x -> print x; print " ") l
+
 let command_line args =
   print "#\n# This Makefile was generated by the command line :\n";
   print "# coq_makefile ";
-  List.iter (fun x -> print x; print " ") args;
+  print_list args;
   print "\n#\n\n"
 
+let directories_deps l =
+  let print_dep f dep = 
+    if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end
+  in
+  let rec iter ((dirs,before) as acc) = function
+    | [] -> 
+	()
+    | (Subdir d) :: l -> 
+	print_dep d before; iter (d::dirs,d::before) l
+    | (ML f) :: l ->
+	print_dep f dirs; iter (dirs,f::before) l
+    | (V f) :: l ->
+	print_dep f dirs; iter (dirs,f::before) l
+    | (Special (f,_,_)) :: l ->
+	print_dep f dirs; iter (dirs,f::before) l
+    | _ :: l -> 
+	iter acc l
+  in
+  iter ([],[]) l
+
 let do_makefile args =
   let l = process_cmd_line args in
   banner ();
@@ -363,6 +385,7 @@ let do_makefile args =
   let sds = subdirs l in
   implicit ();
   standard sds;
+  (* TEST directories_deps l; *)
   warning ();
   if not (!output_channel == stdout) then close_out !output_channel;
   exit 0