src/Pure/GUI/gui_thread.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56773 src/Pure/GUI/swing_thread.scala@5c7ade7a1e74
child 57613 4c6d44a3a079
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Pure/GUI/gui_thread.scala
     2     Module:     PIDE-GUI
     3     Author:     Makarius
     4 
     5 Evaluation within the GUI thread: implementation for AWT/Swing.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import javax.swing.SwingUtilities
    12 
    13 
    14 object GUI_Thread
    15 {
    16   /* context check */
    17 
    18   def assert[A](body: => A) =
    19   {
    20     Predef.assert(SwingUtilities.isEventDispatchThread())
    21     body
    22   }
    23 
    24   def require[A](body: => A) =
    25   {
    26     Predef.require(SwingUtilities.isEventDispatchThread())
    27     body
    28   }
    29 
    30 
    31   /* event dispatch queue */
    32 
    33   def now[A](body: => A): A =
    34   {
    35     if (SwingUtilities.isEventDispatchThread()) body
    36     else {
    37       lazy val result = { assert { Exn.capture(body) } }
    38       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    39       Exn.release(result)
    40     }
    41   }
    42 
    43   def later(body: => Unit)
    44   {
    45     if (SwingUtilities.isEventDispatchThread()) body
    46     else SwingUtilities.invokeLater(new Runnable { def run = body })
    47   }
    48 
    49 
    50   /* delayed events */
    51 
    52   def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    53     Simple_Thread.delay_first(delay) { later { event } }
    54 
    55   def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    56     Simple_Thread.delay_last(delay) { later { event } }
    57 }