more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;
--- a/src/Pure/Build/browser_info.scala Thu Jan 30 21:44:44 2025 +0100
+++ b/src/Pure/Build/browser_info.scala Thu Jan 30 22:29:45 2025 +0100
@@ -51,8 +51,8 @@
}
}
- def init_directory(dir: Path): Path = {
- check_directory(dir)
+ def init_directory(dir: Path, permissive: Boolean = false): Path = {
+ if (!permissive) check_directory(dir)
Isabelle_System.make_directory(dir + PATH)
dir
}
@@ -285,7 +285,7 @@
/* maintain presentation structure */
def update_chapter(session_name: String, session_description: String): Unit = synchronized {
- val dir = Meta_Info.init_directory(chapter_dir(session_name))
+ val dir = Meta_Info.init_directory(chapter_dir(session_name), permissive = true)
Meta_Info.change(dir, Meta_Info.INDEX) { text =>
val index0 = Meta_Info.Index.parse(text, "chapter")
val item = Meta_Info.Item(session_name, description = session_description)
@@ -312,7 +312,7 @@
}
def update_root(): Unit = synchronized {
- Meta_Info.init_directory(root_dir)
+ Meta_Info.init_directory(root_dir, permissive = true)
HTML.init_fonts(root_dir)
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
root_dir + Path.explode("isabelle.gif"))