Holmake: can now (recursively) remove directories in EXTRA_CLEANS

Author: Michael Norrish

tools/Holmake/Holmake.sml

@@ -988,7 +988,7 @@ fun clean_deps() =
 
 fun do_clean_target x = let
   fun clean_action () =
-      Holmake_tools.clean_dir {extra_cleans = extra_cleans()}
+      Holmake_tools.clean_dir outputfns {extra_cleans = extra_cleans()}
 in
   case x of
       "clean" => (info "Cleaning directory of object files\n"; clean_action())

tools/Holmake/Holmake_tools.sig

@@ -76,6 +76,7 @@ sig
       {chattiness:int,
        debug: {ins:string list,outs:string list} option,
        usepfx:bool} -> output_functions
+  val default_ofns : output_functions
   val die_with : string -> 'a
 
 
@@ -99,7 +100,7 @@ sig
   val exists_readable : string -> bool
   val extract_theory : string list -> string option
 
-  val clean_dir : {extra_cleans: string list} -> unit
+  val clean_dir : output_functions -> {extra_cleans: string list} -> unit
   val clean_depdir : {depdirname : string} -> bool
   val clean_forReloc : {holheap : string option} -> unit
   val pushdir : string -> ('a -> 'b) -> ('a -> 'b)

tools/Holmake/Holmake_tools.sml

@@ -224,6 +224,9 @@ in
   {warn = warn, diag = diag, tgtfatal = tgtfatal, info = info, chatty = chatty}
 end
 
+val default_ofns =
+    output_functions {usepfx = true, chattiness = 1, debug = NONE}
+
 fun exists_readable s = OS.FileSys.access(s, [OS.FileSys.A_READ])
 
 fun check_distrib toolname = let
@@ -418,9 +421,55 @@ fun read_files ds P action =
       (if P nextfile then action nextfile else ();
        read_files ds P action)
 
+fun dir_files dnm A =
+    let
+      val ds = OS.FileSys.openDir dnm
+      fun recurse A =
+          case OS.FileSys.readDir ds of
+              NONE => (OS.FileSys.closeDir ds; A)
+            | SOME nm => recurse (OS.Path.concat (dnm, nm) :: A)
+    in
+      recurse A
+    end
+
+fun recursive_act file_act dir_act name =
+    let
+      fun worklist nms rmds =
+          case nms of
+              [] => List.app dir_act rmds
+            | n::ns =>
+              if OS.FileSys.isDir n then
+                worklist (dir_files n ns) (n :: rmds)
+              else (file_act n ; worklist ns rmds)
+    in
+      worklist [name] []
+    end
+
 fun quiet_remove s = OS.FileSys.remove s handle e => ()
+fun chatty_remove act (ofns : output_functions) s =
+    act s handle e =>
+                 (#warn ofns ("Attempt to remove: " ^ s ^
+                              " failed with exception " ^ General.exnMessage e);
+                  raise e)
+
+fun clean1 (ofns : output_functions) s =
+    let val _ = #diag ofns "tools" (fn () => "clean1 " ^ s)
+    in
+      if OS.FileSys.access (s, []) then
+        if OS.FileSys.isDir s then
+          if String.isSuffix "/" s then
+            recursive_act (chatty_remove OS.FileSys.remove ofns)
+                          (chatty_remove OS.FileSys.rmDir ofns)
+                          s
+          else
+            (#warn ofns ("Not removing directory " ^ s ^ " from EXTRA_CLEANS.");
+             #warn ofns ("  Use trailing / on name to force this."))
+        else chatty_remove OS.FileSys.remove ofns s
+      else (* doesn't exist, do nothing *) ()
+    end
+
 
-fun clean_dir {extra_cleans} = let
+fun clean_dir ofns {extra_cleans} = let
   val cdstream = OS.FileSys.openDir "."
   fun to_delete f =
       case (toFile f) of
@@ -434,8 +483,8 @@ fun clean_dir {extra_cleans} = let
       | ART _ => true
       | _ => false
 in
-  read_files cdstream to_delete quiet_remove;
-  app quiet_remove extra_cleans
+  read_files cdstream to_delete (chatty_remove OS.FileSys.remove ofns);
+  app (clean1 ofns) extra_cleans
 end
 
 fun clean_forReloc {holheap} =

tools/buildutils.sml

@@ -446,27 +446,30 @@ fun hmakefile_data HOLDIR =
 
 fun clean0 HOLDIR = let
   val {includes,extra_cleans,...} = hmakefile_data HOLDIR
+  open Holmake_tools
 in
-  Holmake_tools.clean_dir {extra_cleans = extra_cleans} ;
+  clean_dir default_ofns {extra_cleans = extra_cleans} ;
   includes
 end
 
 fun cleanAll0 HOLDIR = let
   val {includes,extra_cleans,...} = hmakefile_data HOLDIR
+  open Holmake_tools
 in
-  Holmake_tools.clean_dir {extra_cleans = extra_cleans};
-  Holmake_tools.clean_depdir {depdirname = ".HOLMK"};
-  Holmake_tools.clean_depdir {depdirname = ".hollogs"};
+  clean_dir default_ofns {extra_cleans = extra_cleans};
+  clean_depdir {depdirname = ".HOLMK"};
+  clean_depdir {depdirname = ".hollogs"};
   includes
 end
 
 fun cleanForReloc0 HOLDIR =
   let
     val {includes,holheap,...} = hmakefile_data HOLDIR
+    open Holmake_tools
   in
-    Holmake_tools.clean_forReloc {holheap = holheap};
-    Holmake_tools.clean_depdir {depdirname = ".HOLMK"};
-    Holmake_tools.clean_depdir {depdirname = ".hollogs"};
+    clean_forReloc {holheap = holheap};
+    clean_depdir {depdirname = ".HOLMK"};
+    clean_depdir {depdirname = ".hollogs"};
     includes
   end