src/Pure/GUI/gui_thread.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 76709 fdbdc573a06b
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56773
diff changeset
     1
/*  Title:      Pure/GUI/gui_thread.scala
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     3
57613
4c6d44a3a079 tuned comments;
wenzelm
parents: 57612
diff changeset
     4
Evaluation within the GUI thread (for AWT/Swing).
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     5
*/
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     6
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     7
package isabelle
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     8
55618
995162143ef4 tuned imports;
wenzelm
parents: 53853
diff changeset
     9
56773
5c7ade7a1e74 removed dead code;
wenzelm
parents: 56770
diff changeset
    10
import javax.swing.SwingUtilities
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    11
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    13
object GUI_Thread {
56773
5c7ade7a1e74 removed dead code;
wenzelm
parents: 56770
diff changeset
    14
  /* context check */
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    16
  def assert[A](body: => A): A = {
71716
wenzelm
parents: 71704
diff changeset
    17
    Predef.assert(SwingUtilities.isEventDispatchThread)
52859
f31624cc4467 tuned signature;
wenzelm
parents: 52477
diff changeset
    18
    body
f31624cc4467 tuned signature;
wenzelm
parents: 52477
diff changeset
    19
  }
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    20
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    21
  def require[A](body: => A): A = {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 71716
diff changeset
    22
    Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected")
52859
f31624cc4467 tuned signature;
wenzelm
parents: 52477
diff changeset
    23
    body
f31624cc4467 tuned signature;
wenzelm
parents: 52477
diff changeset
    24
  }
52477
025b3777e592 tuned signature;
wenzelm
parents: 49251
diff changeset
    25
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    26
56773
5c7ade7a1e74 removed dead code;
wenzelm
parents: 56770
diff changeset
    27
  /* event dispatch queue */
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    28
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    29
  def now[A](body: => A): A = {
71716
wenzelm
parents: 71704
diff changeset
    30
    if (SwingUtilities.isEventDispatchThread) body
48000
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    31
    else {
71716
wenzelm
parents: 71704
diff changeset
    32
      lazy val result = assert { Exn.capture(body) }
wenzelm
parents: 71704
diff changeset
    33
      SwingUtilities.invokeAndWait(() => result)
48000
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    34
      Exn.release(result)
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    35
    }
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    36
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    37
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    38
  def later(body: => Unit): Unit = {
71716
wenzelm
parents: 71704
diff changeset
    39
    if (SwingUtilities.isEventDispatchThread) body
wenzelm
parents: 71704
diff changeset
    40
    else SwingUtilities.invokeLater(() => body)
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    41
  }
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    42
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    43
  def future[A](body: => A): Future[A] = {
71716
wenzelm
parents: 71704
diff changeset
    44
    if (SwingUtilities.isEventDispatchThread) Future.value(body)
67129
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    45
    else {
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    46
      val promise = Future.promise[A]
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    47
      later { promise.fulfill_result(Exn.capture(body)) }
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    48
      promise
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    49
    }
0262a378d5d6 added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents: 66094
diff changeset
    50
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    51
}