changeset 64867 | e7220f4de11f |
parent 64866 | 372c833c7660 |
child 66082 | 2d12a730a380 |
--- a/src/Pure/PIDE/editor.scala Tue Jan 10 16:09:04 2017 +0100 +++ b/src/Pure/PIDE/editor.scala Tue Jan 10 16:53:05 2017 +0100 @@ -10,7 +10,7 @@ abstract class Editor[Context] { def session: Session - def flush(hidden: Boolean = false): Unit + def flush(hidden: Boolean = false, purge: Boolean = false): Unit def invoke(): Unit def invoke_generated(): Unit def current_context: Context