more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
authorwenzelm
Fri, 26 Aug 2022 12:26:58 +0200
changeset 75982 2fff9ce6b460
parent 75981 a1b131d5575f
child 75983 34dd96a06c45
more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Aug 26 12:10:29 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Fri Aug 26 12:26:58 2022 +0200
@@ -57,6 +57,12 @@
       dir
     }
 
+    def clean_directory(dir: Path): Path = {
+      check_directory(dir)
+      Isabelle_System.rm_tree(dir)  // guarded by check_directory!
+      Isabelle_System.new_directory(dir + PATH)
+    }
+
 
     /* content */
 
@@ -532,7 +538,7 @@
     progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
 
     Meta_Data.init_directory(context.chapter_dir(session_name))
-    Meta_Data.init_directory(session_dir)
+    Meta_Data.clean_directory(session_dir)
 
     val session = context.document_info.the_session(session_name)