--- a/src/Pure/PIDE/editor.scala Sat Nov 01 13:58:07 2025 +0100
+++ b/src/Pure/PIDE/editor.scala Sat Nov 01 14:19:16 2025 +0100
@@ -31,6 +31,7 @@
def session: Session
def flush(): Unit
def invoke(): Unit
+ def revoke(): Unit
def get_models(): Iterable[Document.Model]