src/Pure/System/jfx_thread.scala
author wenzelm
Thu, 05 Sep 2013 21:37:32 +0200
changeset 53423 b5a279c7d7f3
parent 49066 1067a639d42a
permissions -rw-r--r--
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/jfx_thread.scala
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
     2
    Module:     PIDE
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
}