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;
     1 /*  Title:      Pure/GUI/gui_thread.scala
     2     Author:     Makarius
     3 
     4 Evaluation within the GUI thread (for AWT/Swing).
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import javax.swing.SwingUtilities
    11 
    12 
    13 object GUI_Thread
    14 {
    15   /* context check */
    16 
    17   def assert[A](body: => A): A =
    18   {
    19     Predef.assert(SwingUtilities.isEventDispatchThread())
    20     body
    21   }
    22 
    23   def require[A](body: => A): A =
    24   {
    25     Predef.require(SwingUtilities.isEventDispatchThread())
    26     body
    27   }
    28 
    29 
    30   /* event dispatch queue */
    31 
    32   def now[A](body: => A): A =
    33   {
    34     if (SwingUtilities.isEventDispatchThread()) body
    35     else {
    36       lazy val result = { assert { Exn.capture(body) } }
    37       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    38       Exn.release(result)
    39     }
    40   }
    41 
    42   def later(body: => Unit)
    43   {
    44     if (SwingUtilities.isEventDispatchThread()) body
    45     else SwingUtilities.invokeLater(new Runnable { def run = body })
    46   }
    47 
    48   def future[A](body: => A): Future[A] =
    49   {
    50     if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    51     else {
    52       val promise = Future.promise[A]
    53       later { promise.fulfill_result(Exn.capture(body)) }
    54       promise
    55     }
    56   }
    57 
    58 
    59   /* delayed events */
    60 
    61   def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
    62     Standard_Thread.delay_first(delay) { later { event } }
    63 
    64   def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
    65     Standard_Thread.delay_last(delay) { later { event } }
    66 }