tuned;
authorwenzelm
Tue, 05 Aug 2025 16:04:05 +0200
changeset 82947 79d14c862560
parent 82946 962b73cc57dc
child 82948 e2e43992f339
tuned;
src/Tools/VSCode/src/vscode_model.scala
src/Tools/jEdit/src/document_model.scala
--- 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))
       }
     }