# HG changeset patch
# User wenzelm
# Date 1751205225 -7200
# Node ID 0bc9dbc61f7f558a797215f21d2b066c8bfa9821
# Parent  3db393729a65801b4702deef20d43187b2ef1a2b
more robust: avoid crash on session database errors;

diff -r 3db393729a65 -r 0bc9dbc61f7f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Jun 29 15:48:13 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Jun 29 15:53:45 2025 +0200
@@ -157,22 +157,27 @@
     theory_name: String,
     theory_node: Document.Node,
   ): Document.Node = {
-    val command = session.read_theory(theory_name)  // FIXME handle errors
+    Exn.capture(session.read_theory(theory_name)) match {
+      case Exn.Res(command) =>
+        val thy_ok = command.source == theory_node.source
+        val blobs_changed =
+          for {
+            case Exn.Res(blob) <- command.blobs
+            (digest, _) <- blob.content
+            doc_blob <- doc_blobs.get(blob.name)
+            if digest != doc_blob.bytes.sha1_digest
+          } yield blob.name
 
-    val thy_ok = command.source == theory_node.source
-    val blobs_changed =
-      for {
-        case Exn.Res(blob) <- command.blobs
-        (digest, _) <- blob.content
-        doc_blob <- doc_blobs.get(blob.name)
-        if digest != doc_blob.bytes.sha1_digest
-      } yield blob.name
+        val command1 =
+          if (thy_ok && blobs_changed.isEmpty) command
+          else command // FIXME errors as markup
 
-    val command1 =
-      if (thy_ok && blobs_changed.isEmpty) command
-      else command // FIXME errors as markup
+        theory_node.update_commands(Linear_Set(command1))
 
-    theory_node.update_commands(Linear_Set(command1))
+      case Exn.Exn(exn) =>
+        session.system_output(Output.error_message_text(Exn.print(exn)))
+        theory_node
+    }
   }