# HG changeset patch
# User wenzelm
# Date 1672840211 -3600
# Node ID e27d097d7d153341965d67257e197d46b9ce2e88
# Parent  f9de9c4b21561ac9437ccb9fc87c91d1c68fa497
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;

diff -r f9de9c4b2156 -r e27d097d7d15 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -428,7 +428,7 @@
   def blobs_info(
     resources: Resources,
     syntax: Outer_Syntax,
-    get_blob: Document.Node.Name => Option[Document.Blob],
+    get_blob: Document.Node.Name => Option[Document.Blobs.Item],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
     span: Command_Span.Span
diff -r f9de9c4b2156 -r e27d097d7d15 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -41,17 +41,17 @@
 
   /* document blobs: auxiliary files */
 
-  sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) {
-    def unchanged: Blob = copy(changed = false)
-  }
+  object Blobs {
+    sealed case class Item(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) {
+      def unchanged: Item = copy(changed = false)
+    }
 
-  object Blobs {
-    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
+    def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs)
     val empty: Blobs = apply(Map.empty)
   }
 
-  final class Blobs private(blobs: Map[Node.Name, Blob]) {
-    def get(name: Node.Name): Option[Blob] = blobs.get(name)
+  final class Blobs private(blobs: Map[Node.Name, Blobs.Item]) {
+    def get(name: Node.Name): Option[Blobs.Item] = blobs.get(name)
 
     def changed(name: Node.Name): Boolean =
       get(name) match {
@@ -171,7 +171,7 @@
           case _ => false
         }
     }
-    case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
+    case class Blob[A, B](blob: Blobs.Item) extends Edit[A, B]
 
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
@@ -264,11 +264,12 @@
 
     val empty: Node = new Node()
 
-    def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
+    def init_blob(blob: Blobs.Item): Node =
+      new Node(get_blob = Some(blob.unchanged))
   }
 
   final class Node private(
-    val get_blob: Option[Document.Blob] = None,
+    val get_blob: Option[Blobs.Item] = None,
     val header: Node.Header = Node.no_header,
     val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
@@ -794,7 +795,7 @@
 
     def node_required: Boolean
 
-    def get_blob: Option[Blob]
+    def get_blob: Option[Blobs.Item]
 
     def untyped_data: AnyRef
     def get_data[C](c: Class[C]): Option[C] = Library.as_subclass(c)(untyped_data)
diff -r f9de9c4b2156 -r e27d097d7d15 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -496,7 +496,7 @@
     }
 
     sealed case class State(
-      blobs: Map[Document.Node.Name, Document.Blob] = Map.empty,
+      blobs: Map[Document.Node.Name, Document.Blobs.Item] = Map.empty,
       theories: Map[Document.Node.Name, Theory] = Map.empty,
       required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty
     ) {
@@ -508,9 +508,9 @@
         val new_blobs =
           names.flatMap { name =>
             val bytes = Bytes.read(name.path)
-            def new_blob: Document.Blob = {
+            def new_blob: Document.Blobs.Item = {
               val text = bytes.text
-              Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true)
+              Document.Blobs.Item(bytes, text, Symbol.Text_Chunk(text), changed = true)
             }
             blobs.get(name) match {
               case Some(blob) if blob.bytes == bytes => None
@@ -524,7 +524,7 @@
 
       def blob_edits(
         name: Document.Node.Name,
-        old_blob: Option[Document.Blob]
+        old_blob: Option[Document.Blobs.Item]
       ) : List[Document.Edit_Text] = {
         val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString)))
         val text_edits =
diff -r f9de9c4b2156 -r e27d097d7d15 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -166,7 +166,7 @@
   private def reparse_spans(
     resources: Resources,
     syntax: Outer_Syntax,
-    get_blob: Document.Node.Name => Option[Document.Blob],
+    get_blob: Document.Node.Name => Option[Document.Blobs.Item],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
     commands: Linear_Set[Command],
@@ -213,7 +213,7 @@
   private def text_edit(
     resources: Resources,
     syntax: Outer_Syntax,
-    get_blob: Document.Node.Name => Option[Document.Blob],
+    get_blob: Document.Node.Name => Option[Document.Blobs.Item],
     can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,
     node: Document.Node,
@@ -303,7 +303,7 @@
   ): Session.Change = {
     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
 
-    def get_blob(name: Document.Node.Name): Option[Document.Blob] =
+    def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] =
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     def can_import(name: Document.Node.Name): Boolean =
diff -r f9de9c4b2156 -r e27d097d7d15 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -142,9 +142,9 @@
 
   /* blob */
 
-  def get_blob: Option[Document.Blob] =
+  def get_blob: Option[Document.Blobs.Item] =
     if (is_theory) None
-    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+    else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
 
   /* data */
diff -r f9de9c4b2156 -r e27d097d7d15 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jan 04 14:35:19 2023 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jan 04 14:50:11 2023 +0100
@@ -433,9 +433,9 @@
     Line.Node_Position(node_name.node,
       Line.Position.zero.advance(content.text.substring(0, offset)))
 
-  def get_blob: Option[Document.Blob] =
+  def get_blob: Option[Document.Blobs.Item] =
     if (is_theory) None
-    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+    else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def untyped_data: AnyRef = content.data
 
@@ -575,7 +575,7 @@
 
     def reset_blob(): Unit = GUI_Thread.require { blob = None }
 
-    def get_blob: Option[Document.Blob] = GUI_Thread.require {
+    def get_blob: Option[Document.Blobs.Item] = GUI_Thread.require {
       if (is_theory) None
       else {
         val (bytes, text, chunk) =
@@ -588,7 +588,7 @@
             x
           }
         val changed = !is_stable
-        Some(Document.Blob(bytes, text, chunk, changed))
+        Some(Document.Blobs.Item(bytes, text, chunk, changed))
       }
     }
 
@@ -617,7 +617,7 @@
   def node_required: Boolean = buffer_state.get_node_required
   def set_node_required(b: Boolean): Unit = buffer_state.set_node_required(b)
 
-  def get_blob: Option[Document.Blob] = buffer_state.get_blob
+  def get_blob: Option[Document.Blobs.Item] = buffer_state.get_blob
   def untyped_data: AnyRef = buffer_state.untyped_data