# HG changeset patch
# User wenzelm
# Date 1375692946 -7200
# Node ID 863581a704a6c89a35ad68e9990ab7c78c99f05a
# Parent  64e3374d5014247274935279d50ca46d6ae48862
avoid repeated PIDE.flush_buffers when manipulating overlays;

diff -r 64e3374d5014 -r 863581a704a6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 02 23:03:59 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 05 10:55:46 2013 +0200
@@ -81,19 +81,11 @@
 
   private var overlays = Document.Overlays.empty
 
-  def add_overlay(command: Command, name: String, args: List[String])
-  {
-    Swing_Thread.required()
-    overlays += ((command, name, args))
-    PIDE.flush_buffers()
-  }
+  def add_overlay(command: Command, name: String, args: List[String]): Unit =
+    Swing_Thread.required { overlays += ((command, name, args)) }
 
-  def remove_overlay(command: Command, name: String, args: List[String])
-  {
-    Swing_Thread.required()
-    overlays -= ((command, name, args))
-    PIDE.flush_buffers()
-  }
+  def remove_overlay(command: Command, name: String, args: List[String]): Unit =
+    Swing_Thread.required { overlays -= ((command, name, args)) }
 
 
   /* perspective */
diff -r 64e3374d5014 -r 863581a704a6 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 23:03:59 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 10:55:46 2013 +0200
@@ -119,6 +119,8 @@
         }
       case None =>
     }
+
+    PIDE.flush_buffers()
   }
 
   private def locate_query()