# HG changeset patch
# User wenzelm
# Date 1672839319 -3600
# Node ID f9de9c4b21561ac9437ccb9fc87c91d1c68fa497
# Parent  2e791bdedec293f6af9b8c8eaa5ba6e5bf503fd5
clarified signature: old node is ignored;

diff -r 2e791bdedec2 -r f9de9c4b2156 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jan 04 14:26:30 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Jan 04 14:35:19 2023 +0100
@@ -263,6 +263,8 @@
     }
 
     val empty: Node = new Node()
+
+    def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
   }
 
   final class Node private(
@@ -292,8 +294,6 @@
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
-    def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
-
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
diff -r 2e791bdedec2 -r f9de9c4b2156 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 14:26:30 2023 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 14:35:19 2023 +0100
@@ -245,7 +245,7 @@
     }
 
     edit match {
-      case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
+      case (_, Document.Node.Blob(blob)) => Document.Node.init_blob(blob)
 
       case (name, Document.Node.Edits(text_edits)) =>
         if (name.is_theory) {