# HG changeset patch
# User wenzelm
# Date 1484060944 -3600
# Node ID 372c833c76606ecfd431bd92bfead28f8ec34d8e
# Parent  778c64c1736314c2a40ed218e5f6568901dd492b
proper template;

diff -r 778c64c17363 -r 372c833c7660 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Jan 10 16:03:50 2017 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Jan 10 16:09:04 2017 +0100
@@ -10,7 +10,7 @@
 abstract class Editor[Context]
 {
   def session: Session
-  def flush(hidden: Boolean = true): Unit
+  def flush(hidden: Boolean = false): Unit
   def invoke(): Unit
   def invoke_generated(): Unit
   def current_context: Context