more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;
authorwenzelm
Thu, 30 Jan 2025 22:29:45 +0100
changeset 82023 9601f5582f33
parent 82022 337d3bb65325
child 82024 bbda3b4f3c99
more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;
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"))