diff -r 372c833c7660 -r e7220f4de11f src/Pure/PIDE/editor.scala
--- 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