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