# HG changeset patch
# User wenzelm
# Date 1661087786 -7200
# Node ID 32c4f87668314055f6896fb09241c4111b9996c7
# Parent  864b10457a7d40130166a053ff8ff30c6d2c9cd9
clarified synchronized operations: approximate file-system transactions;

diff -r 864b10457a7d -r 32c4f8766831 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 15:00:14 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 15:16:26 2022 +0200
@@ -166,31 +166,37 @@
 
     private val sessions_path = Path.basic(".sessions")
 
-    private def read_sessions(dir: Path): List[(String, String)] = synchronized {
-      val path = dir + sessions_path
-      if (path.is_file) {
-        import XML.Decode._
-        list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
-      }
-      else Nil
-    }
-
-    def update_chapter(chapter: String, new_sessions: List[(String, String)]): Unit = synchronized {
-      val dir = Isabelle_System.make_directory(root_dir + Path.basic(chapter))
+    private def update_sessions_list(
+      chapter_dir: Path,
+      new_sessions: List[(String, String)]
+    ): List[(String, String)] = synchronized {
+      val path = chapter_dir + sessions_path
 
       val sessions0 =
-        try { read_sessions(dir) }
-        catch { case _: XML.Error => Nil }
+        if (path.is_file) {
+          import XML.Decode._
+          list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
+        }
+        else Nil
 
       val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
-      File.write(dir + sessions_path,
+
+      File.write(path,
         {
           import XML.Encode._
           YXML.string_of_body(list(pair(string, string))(sessions))
         })
 
+      sessions
+    }
+
+    def update_chapter(chapter: String, new_sessions: List[(String, String)]): Unit = synchronized {
+      val chapter_dir = Isabelle_System.make_directory(root_dir + Path.basic(chapter))
+
+      val sessions = update_sessions_list(chapter_dir, new_sessions)
+
       val title = "Isabelle/" + chapter + " sessions"
-      HTML.write_document(dir, "index.html",
+      HTML.write_document(chapter_dir, "index.html",
         List(HTML.title(title + Isabelle_System.isabelle_heading())),
         HTML.chapter(title) ::
          (if (sessions.isEmpty) Nil