src/Pure/GUI/jfx_gui.scala
author blanchet
Thu, 05 Mar 2015 11:57:34 +0100
changeset 59597 70a68edcc79b
parent 57908 1937603dbdf2
child 59720 f893472fff31
permissions -rw-r--r--
helpful error message when 'auto' fails
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
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
     2
    Module:     PIDE-JFX
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
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
     5
Basic GUI tools (for Java FX).
49065
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
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    11
import java.io.{FileInputStream, BufferedInputStream}
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    12
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    13
import javafx.application.{Platform => JFX_Platform}
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    14
import javafx.scene.text.{Font => JFX_Font}
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    15
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    16
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    17
object JFX_GUI
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    18
{
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    19
  /* evaluation within the Java FX application thread */
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    20
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    21
  object Thread
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    22
  {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    23
    def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    24
    def require() = Predef.require(JFX_Platform.isFxApplicationThread())
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    25
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    26
    def later(body: => Unit)
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    27
    {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    28
      if (JFX_Platform.isFxApplicationThread()) body
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    29
      else JFX_Platform.runLater(new Runnable { def run = body })
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    30
    }
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    31
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    32
    def future[A](body: => A): Future[A] =
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    33
    {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    34
      if (JFX_Platform.isFxApplicationThread()) Future.value(body)
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    35
      else {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    36
        val promise = Future.promise[A]
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    37
        later { promise.fulfill_result(Exn.capture(body)) }
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    38
        promise
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    39
      }
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    40
    }
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    41
  }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    42
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    43
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    44
  /* Isabelle fonts */
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    45
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    46
  def install_fonts()
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    47
  {
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    48
    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    49
      val stream = new BufferedInputStream(new FileInputStream(font.file))
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    50
      try { JFX_Font.loadFont(stream, 1.0) }
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    51
      finally { stream.close }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    52
    }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    53
  }
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    54
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    55
}