--- a/src/Pure/PIDE/editor.scala Mon Oct 27 12:37:31 2025 +0100
+++ b/src/Pure/PIDE/editor.scala Mon Oct 27 15:16:32 2025 +0100
@@ -16,6 +16,7 @@
}
sealed case class Output(
+ snapshot: Document.Snapshot = Document.Snapshot.init,
results: Command.Results = Command.Results.empty,
messages: List[XML.Elem] = Nil,
defined: Boolean = true
@@ -138,7 +139,7 @@
val (urgent, regular) = other.partition(Protocol.is_urgent)
urgent ::: (if (output_state()) states else Nil) ::: regular
}
- Editor.Output(results = results, messages = messages)
+ Editor.Output(snapshot = snapshot, results = results, messages = messages)
}
else Editor.Output.none
}