# HG changeset patch
# User wenzelm
# Date 1754481976 -7200
# Node ID 7185406956cd1d513310c251d88db0e4b5b80734
# Parent  1d6dc0eef4cfcbf5553fc2bcc100c478483a7e60
proper comparison of actual source (amending fe8598c92be7), e.g. relevant for "File / Reload with Encoding / UTF-8" in Isabelle/jEdit;

diff -r 1d6dc0eef4cf -r 7185406956cd src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Aug 06 13:25:41 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Aug 06 14:06:16 2025 +0200
@@ -157,23 +157,23 @@
       store, resources.session_background, document_snapshot = document_snapshot)
   }
 
-  private val read_theory_cache = new WeakHashMap[String, WeakReference[Command]]
+  private val read_theory_cache = new WeakHashMap[String, WeakReference[Document.Snapshot]]
 
-  def read_theory(name: String): Command =
+  def read_theory(name: String): Document.Snapshot =
     read_theory_cache.synchronized {
       Option(read_theory_cache.get(name)).map(_.get) match {
-        case Some(command: Command) => command
+        case Some(snapshot: Document.Snapshot) => snapshot
         case _ =>
-          val snapshot =
+          val maybe_snapshot =
             using(open_session_context()) { session_context =>
               Build.read_theory(session_context.theory(name),
                 unicode_symbols = true,
                 migrate_file = (a: String) => session.resources.append_path("", Path.explode(a)))
             }
-          snapshot.map(_.snippet_commands) match {
-            case Some(List(command)) =>
-              read_theory_cache.put(name, new WeakReference(command))
-              command
+          maybe_snapshot.map(_.snippet_commands) match {
+            case Some(List(_)) =>
+              read_theory_cache.put(name, new WeakReference(maybe_snapshot.get))
+              maybe_snapshot.get
             case _ => error("Failed to load theory " + quote(name) + " from session database")
           }
       }
diff -r 1d6dc0eef4cf -r 7185406956cd src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 13:25:41 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 14:06:16 2025 +0200
@@ -161,18 +161,20 @@
     val theory = node_name.theory
 
     Exn.capture(session.read_theory(theory)) match {
-      case Exn.Res(command) =>
+      case Exn.Res(snapshot) =>
+        val command = snapshot.snippet_commands.head
         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
+              List.from(
+                for {
+                  blob_name <- command.blobs_names.iterator
+                  blob_node = snapshot.version.nodes(blob_name)
+                  doc_blob <- doc_blobs.get(blob_name)
+                  if blob_node.source != doc_blob.source
+                } yield blob_name.node)
 
             val changed = thy_changed ::: blobs_changed
             val command1 =