# HG changeset patch # User wenzelm # Date 1375693277 -7200 # Node ID f31624cc446778def31feea5aece917ee23cc6ce # Parent 863581a704a6c89a35ad68e9990ab7c78c99f05a tuned signature; diff -r 863581a704a6 -r f31624cc4467 src/Pure/System/swing_thread.scala --- 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 */ diff -r 863581a704a6 -r f31624cc4467 src/Tools/jEdit/src/document_model.scala --- 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 */ diff -r 863581a704a6 -r f31624cc4467 src/Tools/jEdit/src/pretty_tooltip.scala --- 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()