From 728bbdd770b0d3e1e09fadef33451327bc5e742b Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 22 Jun 2012 15:57:26 +0000
Subject: Refactoring seems OK

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15477 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coq_makefile.ml | 83 +++++++++++++++++++++++++--------------------------
 1 file changed, 40 insertions(+), 43 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 462152a51..654bb3981 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -179,65 +179,62 @@ let install_include_by_root =
       printf "\tdone\n";
       install_inc_i b)
 
-let install_doc some_vfiles some_mlifiles (_,inc_r) =
-  let install_one_kind kind dir =
-    printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind;
-    printf "\tfor i in %s/*; do \\\n" kind;
-    printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
-    print "\tdone\n" in
-    print "install-doc:\n";
-    let () = match inc_r with
-      |[] ->
-	 if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
-	  if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
-      |(_,lp,_)::q ->
-	 let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-	   if (pr <> "") &&
-	     ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.')
-	   then begin
-	     let rt = physical_dir_of_logical_dir pr in
-	       if some_vfiles then install_one_kind "html" rt;
-	       if some_mlifiles then install_one_kind "mlihtml" rt;
-	   end else begin
-	     prerr_string "Warning: -R options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n";
-	   if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
-	   if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
-	   end in
-      print "\n"
+let where_put_doc = function
+    |_,[] -> "$(INSTALLDEFAULTROOT)";
+    |_,((_,lp,_)::q as inc_r) ->
+      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
+      if (pr <> "") &&
+	((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.')
+      then
+	physical_dir_of_logical_dir pr
+      else
+	let () = prerr_string "Warning: -R options don't have a correct common prefix,
+ install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+	"$(INSTALLDEFAULTROOT)"
 
 let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function
-  |Project_file.NoInstall -> ()
+  |Project_file.NoInstall -> None
   |is_install ->
+    let not_empty = function |[] -> false |_::_ -> true in
+    let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in
+    let cmifiles = List.rev_append mlifiles cmofiles in
+    let cmxsfiles = List.rev_append cmofiles mllibfiles in
+    let where_what_cmxs = vars_to_put_by_root [] "CMXSFILES" cmxsfiles inc in
+    let where_what =
+      vars_to_put_by_root (
+	vars_to_put_by_root (
+	  vars_to_put_by_root (
+	    vars_to_put_by_root [] "VOFILES" vfiles inc
+	  ) "CMOFILES" cmofiles inc
+	) "CMIFILES" cmifiles inc
+      ) "CMAFILES" mllibfiles inc in
+    let doc_dir = where_put_doc inc in
     let () = if is_install = Project_file.UnspecInstall then
 	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in
-    let not_empty = function |[] -> false |_::_ -> true in
-    let cmofiles = mlpackfiles@mlfiles@ml4files in
-    let cmifiles = mlifiles@cmofiles in
-    let cmxsfiles = cmofiles@mllibfiles in
     if (not_empty cmxsfiles) then begin
       print "install-natdynlink:\n";
-      install_include_by_root (vars_to_put_by_root [] "CMXSFILES" cmxsfiles inc);
+      install_include_by_root where_what_cmxs;
       print "\n";
     end;
     print "install:";
     if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)";
     print "\n";
-    let sorted_dirs =
-      vars_to_put_by_root (
-	vars_to_put_by_root (
-	  vars_to_put_by_root (
-	    vars_to_put_by_root [] "VOFILES" vfiles inc
-	  ) "CMOFILES" cmofiles inc
-	) "CMIFILES" cmifiles inc
-      ) "CMAFILES" mllibfiles inc in
-    install_include_by_root sorted_dirs;
+    install_include_by_root where_what;
     List.iter
       (fun x ->
-	 printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
+	printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
       sds;
     print "\n";
-    install_doc (not_empty vfiles) (not_empty mlifiles) inc
+    let install_one_kind kind dir =
+      printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind;
+      printf "\tfor i in %s/*; do \\\n" kind;
+      printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
+      print "\tdone\n" in
+    print "install-doc:\n";
+    if not_empty vfiles then install_one_kind "html" doc_dir;
+    if not_empty mlifiles then install_one_kind "mlihtml" doc_dir;
+    print "\n";
+    Some (List.rev_append where_what_cmxs where_what,doc_dir)
 
 let make_makefile sds =
   if !make_name <> "" then begin
-- 
cgit v1.2.3