clarified signature: old node is ignored;

--- 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)
 

--- 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) {