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