src/Pure/GUI/gui_thread.scala
author wenzelm
Mon Dec 04 21:23:56 2017 +0100 (16 months ago)
changeset 67129 0262a378d5d6
parent 66094 24658c9d7c78
permissions -rw-r--r--
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm@57612
     1
/*  Title:      Pure/GUI/gui_thread.scala
wenzelm@29202
     2
    Author:     Makarius
wenzelm@29202
     3
wenzelm@57613
     4
Evaluation within the GUI thread (for AWT/Swing).
wenzelm@29202
     5
*/
wenzelm@29202
     6
wenzelm@29202
     7
package isabelle
wenzelm@29202
     8
wenzelm@55618
     9
wenzelm@56773
    10
import javax.swing.SwingUtilities
wenzelm@31942
    11
wenzelm@29202
    12
wenzelm@57612
    13
object GUI_Thread
wenzelm@29202
    14
{
wenzelm@56773
    15
  /* context check */
wenzelm@32494
    16
wenzelm@66094
    17
  def assert[A](body: => A): A =
wenzelm@52859
    18
  {
wenzelm@52859
    19
    Predef.assert(SwingUtilities.isEventDispatchThread())
wenzelm@52859
    20
    body
wenzelm@52859
    21
  }
wenzelm@32494
    22
wenzelm@66094
    23
  def require[A](body: => A): A =
wenzelm@52859
    24
  {
wenzelm@52859
    25
    Predef.require(SwingUtilities.isEventDispatchThread())
wenzelm@52859
    26
    body
wenzelm@52859
    27
  }
wenzelm@52477
    28
wenzelm@32494
    29
wenzelm@56773
    30
  /* event dispatch queue */
wenzelm@31942
    31
wenzelm@34026
    32
  def now[A](body: => A): A =
wenzelm@34026
    33
  {
wenzelm@48000
    34
    if (SwingUtilities.isEventDispatchThread()) body
wenzelm@48000
    35
    else {
wenzelm@56662
    36
      lazy val result = { assert { Exn.capture(body) } }
wenzelm@48000
    37
      SwingUtilities.invokeAndWait(new Runnable { def run = result })
wenzelm@48000
    38
      Exn.release(result)
wenzelm@48000
    39
    }
wenzelm@29649
    40
  }
wenzelm@29202
    41
wenzelm@34299
    42
  def later(body: => Unit)
wenzelm@34299
    43
  {
wenzelm@32494
    44
    if (SwingUtilities.isEventDispatchThread()) body
wenzelm@29649
    45
    else SwingUtilities.invokeLater(new Runnable { def run = body })
wenzelm@29649
    46
  }
wenzelm@31942
    47
wenzelm@67129
    48
  def future[A](body: => A): Future[A] =
wenzelm@67129
    49
  {
wenzelm@67129
    50
    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
wenzelm@67129
    51
    else {
wenzelm@67129
    52
      val promise = Future.promise[A]
wenzelm@67129
    53
      later { promise.fulfill_result(Exn.capture(body)) }
wenzelm@67129
    54
      promise
wenzelm@67129
    55
    }
wenzelm@67129
    56
  }
wenzelm@67129
    57
wenzelm@31942
    58
wenzelm@56770
    59
  /* delayed events */
wenzelm@49195
    60
wenzelm@62263
    61
  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
wenzelm@62263
    62
    Standard_Thread.delay_first(delay) { later { event } }
wenzelm@49196
    63
wenzelm@62263
    64
  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
wenzelm@62263
    65
    Standard_Thread.delay_last(delay) { later { event } }
wenzelm@29202
    66
}