src/Tools/jEdit/src/pretty_tooltip.scala
changeset 57612 990ffb84489b
parent 56930 42b5d216dc8c
child 57849 6d8f97d555d8
     1.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -25,19 +25,19 @@
     1.4  {
     1.5    /* tooltip hierarchy */
     1.6  
     1.7 -  // owned by Swing thread
     1.8 +  // owned by GUI thread
     1.9    private var stack: List[Pretty_Tooltip] = Nil
    1.10  
    1.11    private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
    1.12    {
    1.13 -    Swing_Thread.require {}
    1.14 +    GUI_Thread.require {}
    1.15  
    1.16      if (stack.contains(tip)) Some(stack.span(_ != tip))
    1.17      else None
    1.18    }
    1.19  
    1.20    private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
    1.21 -    Swing_Thread.require { stack.find(tip => tip.original_parent == parent) }
    1.22 +    GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
    1.23  
    1.24    def apply(
    1.25      view: View,
    1.26 @@ -47,7 +47,7 @@
    1.27      results: Command.Results,
    1.28      info: Text.Info[XML.Body])
    1.29    {
    1.30 -    Swing_Thread.require {}
    1.31 +    GUI_Thread.require {}
    1.32  
    1.33      stack match {
    1.34        case top :: _ if top.results == results && top.info == info =>
    1.35 @@ -71,13 +71,13 @@
    1.36    }
    1.37  
    1.38  
    1.39 -  /* pending event and active state */  // owned by Swing thread
    1.40 +  /* pending event and active state */  // owned by GUI thread
    1.41  
    1.42    private var pending: Option[() => Unit] = None
    1.43    private var active = true
    1.44  
    1.45    private val pending_delay =
    1.46 -    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
    1.47 +    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
    1.48        pending match {
    1.49          case Some(body) => pending = None; body()
    1.50          case None =>
    1.51 @@ -85,7 +85,7 @@
    1.52      }
    1.53  
    1.54    def invoke(body: () => Unit): Unit =
    1.55 -    Swing_Thread.require {
    1.56 +    GUI_Thread.require {
    1.57        if (active) {
    1.58          pending = Some(body)
    1.59          pending_delay.invoke()
    1.60 @@ -93,18 +93,18 @@
    1.61      }
    1.62  
    1.63    def revoke(): Unit =
    1.64 -    Swing_Thread.require {
    1.65 +    GUI_Thread.require {
    1.66        pending = None
    1.67        pending_delay.revoke()
    1.68      }
    1.69  
    1.70    private lazy val reactivate_delay =
    1.71 -    Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
    1.72 +    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
    1.73        active = true
    1.74      }
    1.75  
    1.76    private def deactivate(): Unit =
    1.77 -    Swing_Thread.require {
    1.78 +    GUI_Thread.require {
    1.79        revoke()
    1.80        active = false
    1.81        reactivate_delay.invoke()
    1.82 @@ -113,7 +113,7 @@
    1.83  
    1.84    /* dismiss */
    1.85  
    1.86 -  private lazy val focus_delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.87 +  private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.88    {
    1.89      dismiss_unfocused()
    1.90    }
    1.91 @@ -173,7 +173,7 @@
    1.92  {
    1.93    tip =>
    1.94  
    1.95 -  Swing_Thread.require {}
    1.96 +  GUI_Thread.require {}
    1.97  
    1.98  
    1.99    /* controls */