src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Sat Nov 21 20:12:36 2015 +0100
+++ b/src/Pure/PIDE/editor.scala	Sat Nov 21 20:13:52 2015 +0100
@@ -10,7 +10,7 @@
 abstract class Editor[Context]
 {
   def session: Session
-  def flush(): Unit
+  def flush(hidden: Boolean = true): Unit
   def invoke(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]