diff -r 6b2f3eafdf26 -r 0556adb3581b src/Pure/PIDE/editor.scala --- 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]