--- a/src/Tools/VSCode/src/vscode_model.scala Mon Aug 04 13:34:41 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala Tue Aug 05 16:04:05 2025 +0200
@@ -144,7 +144,10 @@
def get_blob: Option[Document.Blobs.Item] =
if (is_theory) None
- else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+ else {
+ val changed = pending_edits.nonEmpty
+ Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, changed = changed))
+ }
/* data */
--- a/src/Tools/jEdit/src/document_model.scala Mon Aug 04 13:34:41 2025 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Aug 05 16:04:05 2025 +0200
@@ -439,7 +439,10 @@
def get_blob: Option[Document.Blobs.Item] =
if (is_theory) None
- else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+ else {
+ val changed = pending_edits.nonEmpty
+ Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, changed = changed))
+ }
def untyped_data: AnyRef = content.data
@@ -596,8 +599,7 @@
blob = Some(x)
x
}
- val changed = !is_stable
- Some(Document.Blobs.Item(bytes, text, chunk, changed))
+ Some(Document.Blobs.Item(bytes, text, chunk, changed = !is_stable))
}
}