tuned signature;
authorwenzelm
Mon, 05 Aug 2013 11:01:17 +0200
changeset 52859 f31624cc4467
parent 52858 863581a704a6
child 52860 f155c38242c1
tuned signature;
src/Pure/System/swing_thread.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/pretty_tooltip.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 */
--- 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()