src/Pure/GUI/jfx_thread.scala
author wenzelm
Sun, 22 Sep 2013 14:30:34 +0200
changeset 53783 f5e9d182f645
parent 49066 src/Pure/System/jfx_thread.scala@1067a639d42a
child 53853 e8430d668f44
permissions -rw-r--r--
clarified location of GUI modules (which depend on Swing of JFX);
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
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     3
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     4
Evaluation within the Java FX application thread.
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     5
*/
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     6
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     7
package isabelle
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     8
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     9
import javafx.application.{Platform => JFX_Platform}
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    10
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    11
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    12
object JFX_Thread
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    13
{
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    14
  /* checks */
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    15
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    16
  def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    17
  def require() = Predef.require(JFX_Platform.isFxApplicationThread())
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    18
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    19
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    20
  /* asynchronous context switch */
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    21
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    22
  def later(body: => Unit)
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    23
  {
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    24
    if (JFX_Platform.isFxApplicationThread()) body
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    25
    else JFX_Platform.runLater(new Runnable { def run = body })
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    26
  }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    27
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    28
  def future[A](body: => A): Future[A] =
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    29
  {
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    30
    if (JFX_Platform.isFxApplicationThread()) Future.value(body)
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    31
    else {
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    32
      val promise = Future.promise[A]
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    33
      later { promise.fulfill_result(Exn.capture(body)) }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    34
      promise
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    35
    }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    36
  }
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    37
}