avoid repeated PIDE.flush_buffers when manipulating overlays;

--- 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 */

--- 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()