# HG changeset patch
# User wenzelm
# Date 1661509618 -7200
# Node ID 2fff9ce6b460c64c62f72c9ea844d24d8c94c061
# Parent  a1b131d5575fdee5fb4686cc03ab986038abcf6a
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();

diff -r a1b131d5575f -r 2fff9ce6b460 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)