src/Pure/GUI/jfx_gui.scala
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 60033 9a1d40876e9f
child 65083 9a0e34edfad1
permissions -rw-r--r--
clarified mode of ROOT.ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 57908
diff changeset
     1
/*  Title:      Pure/GUI/jfx_gui.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
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
     4
Basic GUI tools (for Java FX).
49065
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
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    10
import java.io.{FileInputStream, BufferedInputStream}
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    11
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    12
import javafx.application.{Platform => JFX_Platform}
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    13
import javafx.scene.text.{Font => JFX_Font}
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    14
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    15
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    16
object JFX_GUI
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    17
{
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    18
  /* 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
    19
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    20
  object Thread
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    21
  {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    22
    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
    23
    def require() = Predef.require(JFX_Platform.isFxApplicationThread())
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    24
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    25
    def later(body: => Unit)
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    26
    {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    27
      if (JFX_Platform.isFxApplicationThread()) body
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    28
      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
    29
    }
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
    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
    32
    {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    33
      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
    34
      else {
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    35
        val promise = Future.promise[A]
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    36
        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
    37
        promise
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    38
      }
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    39
    }
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    40
  }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    41
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    42
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    43
  /* Isabelle fonts */
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    44
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    45
  def install_fonts()
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    46
  {
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    47
    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
    48
      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
    49
      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
    50
      finally { stream.close }
49066
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    51
    }
1067a639d42a basic setup for HTML5 panel;
wenzelm
parents: 49065
diff changeset
    52
  }
57908
1937603dbdf2 separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents: 53853
diff changeset
    53
49065
8ead9e8b15fb basic support for Java FX;
wenzelm
parents:
diff changeset
    54
}