# HG changeset patch
# User wenzelm
# Date 1738272585 -3600
# Node ID 9601f5582f33544199fa8de854952abe43320974
# Parent  337d3bb653257102b18cf41533f4f50d355edc9a
more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;

diff -r 337d3bb65325 -r 9601f5582f33 src/Pure/Build/browser_info.scala
--- 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"))