src/Pure/GUI/jfx_thread.scala
author wenzelm
Tue, 24 Sep 2013 20:41:28 +0200
changeset 53853 e8430d668f44
parent 53783 f5e9d182f645
permissions -rw-r--r--
more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53783
f5e9d182f645 clarified location of GUI modules (which depend on Swing of JFX);
wenzelm
parents: 49066
diff changeset
     1
/*  Title:      Pure/GUI/jfx_thread.scala
53853
e8430d668f44 more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
wenzelm
parents: 53783
diff changeset
     2
    Module:     PIDE-GUI
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     4
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     5
Evaluation within the Java FX application thread.
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     6
*/
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     7
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     8
package isabelle
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     9
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    10
import javafx.application.{Platform => JFX_Platform}
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    11
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    12
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    13
object JFX_Thread
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    14
{
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    15
  /* checks */
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    16
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    17
  def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    18
  def require() = Predef.require(JFX_Platform.isFxApplicationThread())
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    19
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    20
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    21
  /* asynchronous context switch */
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    22
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    23
  def later(body: => Unit)
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    24
  {
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    25
    if (JFX_Platform.isFxApplicationThread()) body
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    26
    else JFX_Platform.runLater(new Runnable { def run = body })
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    27
  }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    28
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    29
  def future[A](body: => A): Future[A] =
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    30
  {
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    31
    if (JFX_Platform.isFxApplicationThread()) Future.value(body)
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    32
    else {
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    33
      val promise = Future.promise[A]
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    34
      later { promise.fulfill_result(Exn.capture(body)) }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    35
      promise
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    36
    }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    37
  }
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    38
}