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();
--- 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)