diff -r c7849fa2ece0 -r b51e4a526897 src/Pure/PIDE/editor.scala --- 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 }