# HG changeset patch
# User wenzelm
# Date 1753968049 -7200
# Node ID fb5f91782133fd96c6ae55fde81429afaa4d6c06
# Parent  f170ec047460434aedfec73cf04d44d590c6d34a
proper handling of removed nodes, e.g. via "Theories / Purge" in Isabelle/jEdit;

diff -r f170ec047460 -r fb5f91782133 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Jul 31 15:19:20 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Jul 31 15:20:49 2025 +0200
@@ -162,32 +162,36 @@
 
     Exn.capture(session.read_theory(theory)) match {
       case Exn.Res(command) =>
-        val thy_changed =
-          if (node.source.isEmpty || node.source == command.source) Nil
-          else List(node_name.node)
-        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.node
+        val node_commands =
+          if (node.is_empty) Linear_Set.empty
+          else {
+            val thy_changed = if (node.source == command.source) Nil else List(node_name.node)
+            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.node
 
-        val changed = thy_changed ::: blobs_changed
-        val command1 =
-          if (changed.isEmpty) command
-          else {
-            val node_range = Text.Range(0, Symbol.length(node.source))
-            val msg =
-              XML.Elem(Markup.Bad(Document_ID.make()),
-                XML.string("Changed sources for loaded theory " + quote(theory) +
-                  ":\n" + cat_lines(changed.map(a => "  " + quote(a)))))
-            Command.unparsed(node.source, theory = true, id = command.id, node_name = node_name,
-              blobs_info = command.blobs_info,
-              markups = Command.Markups.empty.add(Text.Info(node_range, msg)))
+            val changed = thy_changed ::: blobs_changed
+            val command1 =
+              if (changed.isEmpty) command
+              else {
+                val node_range = Text.Range(0, Symbol.length(node.source))
+                val msg =
+                  XML.Elem(Markup.Bad(Document_ID.make()),
+                    XML.string("Changed sources for loaded theory " + quote(theory) +
+                      ":\n" + cat_lines(changed.map(a => "  " + quote(a)))))
+                Command.unparsed(node.source, theory = true, id = command.id, node_name = node_name,
+                  blobs_info = command.blobs_info,
+                  markups = Command.Markups.empty.add(Text.Info(node_range, msg)))
+              }
+
+            Linear_Set(command1)
           }
 
-        node.update_commands(Linear_Set(command1))
+        node.update_commands(node_commands)
 
       case Exn.Exn(exn) =>
         session.system_output(Output.error_message_text(Exn.print(exn)))