| author | wenzelm | 
| Wed, 17 May 2017 23:05:30 +0200 | |
| changeset 65860 | ce6be2e40d47 | 
| parent 65083 | 9a0e34edfad1 | 
| permissions | -rw-r--r-- | 
| 59720 | 1 | /* Title: Pure/GUI/jfx_gui.scala | 
| 49065 | 2 | Author: Makarius | 
| 3 | ||
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 4 | Basic GUI tools (for Java FX). | 
| 49065 | 5 | */ | 
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 10 | import java.io.{FileInputStream, BufferedInputStream}
 | 
| 49065 | 11 | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 12 | import javafx.application.{Platform => JFX_Platform}
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 13 | import javafx.scene.text.{Font => JFX_Font}
 | 
| 49065 | 14 | |
| 15 | ||
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 16 | object JFX_GUI | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 17 | {
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 18 | /* evaluation within the Java FX application thread */ | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 19 | |
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 20 | object Thread | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 21 |   {
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 22 | def assert() = Predef.assert(JFX_Platform.isFxApplicationThread()) | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 23 | def require() = Predef.require(JFX_Platform.isFxApplicationThread()) | 
| 49065 | 24 | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 25 | def later(body: => Unit) | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 26 |     {
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 27 | if (JFX_Platform.isFxApplicationThread()) body | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
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: 
53853diff
changeset | 29 | } | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 30 | |
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 31 | def future[A](body: => A): Future[A] = | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 32 |     {
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 33 | if (JFX_Platform.isFxApplicationThread()) Future.value(body) | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 34 |       else {
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 35 | val promise = Future.promise[A] | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 36 |         later { promise.fulfill_result(Exn.capture(body)) }
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 37 | promise | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 38 | } | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 39 | } | 
| 49065 | 40 | } | 
| 49066 | 41 | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 42 | |
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 43 | /* Isabelle fonts */ | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 44 | |
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 45 | def install_fonts() | 
| 49066 | 46 |   {
 | 
| 65083 | 47 |     for (font <- Isabelle_System.fonts()) {
 | 
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
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: 
53853diff
changeset | 49 |       try { JFX_Font.loadFont(stream, 1.0) }
 | 
| 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 50 |       finally { stream.close }
 | 
| 49066 | 51 | } | 
| 52 | } | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
53853diff
changeset | 53 | |
| 49065 | 54 | } |