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