--- a/src/Pure/System/swing_thread.scala Mon Aug 05 10:55:46 2013 +0200
+++ b/src/Pure/System/swing_thread.scala Mon Aug 05 11:01:17 2013 +0200
@@ -16,10 +16,17 @@
{
/* checks */
- def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
- def require() = Predef.require(SwingUtilities.isEventDispatchThread())
+ def assert[A](body: => A) =
+ {
+ Predef.assert(SwingUtilities.isEventDispatchThread())
+ body
+ }
- def required[A](body: => A): A = { require(); body }
+ def require[A](body: => A) =
+ {
+ Predef.require(SwingUtilities.isEventDispatchThread())
+ body
+ }
/* main dispatch queue */
--- a/src/Tools/jEdit/src/document_model.scala Mon Aug 05 10:55:46 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 05 11:01:17 2013 +0200
@@ -82,10 +82,10 @@
private var overlays = Document.Overlays.empty
def add_overlay(command: Command, name: String, args: List[String]): Unit =
- Swing_Thread.required { overlays += ((command, name, args)) }
+ Swing_Thread.require { overlays += ((command, name, args)) }
def remove_overlay(command: Command, name: String, args: List[String]): Unit =
- Swing_Thread.required { overlays -= ((command, name, args)) }
+ Swing_Thread.require { overlays -= ((command, name, args)) }
/* perspective */
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Aug 05 10:55:46 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Aug 05 11:01:17 2013 +0200
@@ -78,7 +78,7 @@
}
def invoke(body: () => Unit): Unit =
- Swing_Thread.required {
+ Swing_Thread.require {
if (active) {
pending = Some(body)
pending_delay.invoke()
@@ -86,7 +86,7 @@
}
def revoke(): Unit =
- Swing_Thread.required {
+ Swing_Thread.require {
pending = None
pending_delay.revoke()
}
@@ -97,7 +97,7 @@
}
private def deactivate(): Unit =
- Swing_Thread.required {
+ Swing_Thread.require {
revoke()
active = false
reactivate_delay.invoke()