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