# HG changeset patch # User wenzelm # Date 1526031743 -7200 # Node ID 7b995cd6d5d4a97ee85d07b161da0e20387b8a94 # Parent 58c9231c293754572151adca8225d56c554625d5 removed unused Java FX modules (it will be unbundled from JDK eventually); diff -r 58c9231c2937 -r 7b995cd6d5d4 src/Pure/GUI/html5_panel.scala --- a/src/Pure/GUI/html5_panel.scala Thu May 10 22:03:51 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -/* Title: Pure/GUI/html5_panel.scala - Author: Makarius - -HTML5 panel based on Java FX WebView. -*/ - -package isabelle - - -import javafx.scene.Scene -import javafx.scene.web.{WebView, WebEngine} -import javafx.scene.input.KeyEvent -import javafx.scene.text.FontSmoothingType -import javafx.scene.layout.{HBox, VBox, Priority} -import javafx.geometry.{HPos, VPos, Insets} -import javafx.event.EventHandler - - -// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414 -// and http://hg.netbeans.org/jet-main/rev/a88434cec458 -private class Web_View_Workaround extends javafx.scene.layout.Pane -{ - VBox.setVgrow(this, Priority.ALWAYS) - HBox.setHgrow(this, Priority.ALWAYS) - - setMaxWidth(java.lang.Double.MAX_VALUE) - setMaxHeight(java.lang.Double.MAX_VALUE) - - val web_view = new WebView - web_view.setMinSize(500, 400) - web_view.setPrefSize(500, 400) - - getChildren().add(web_view) - - override protected def layoutChildren() - { - val managed = getManagedChildren() - val width = getWidth() - val height = getHeight() - val top = getInsets().getTop() - val right = getInsets().getRight() - val left = getInsets().getLeft() - val bottom = getInsets().getBottom() - - for (i <- 0 until managed.size) - layoutInArea(managed.get(i), left, top, - width - left - right, height - top - bottom, - 0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER) - } -} - - -class HTML5_Panel extends javafx.embed.swing.JFXPanel -{ - private val future = - JFX_GUI.Thread.future { - val pane = new Web_View_Workaround - - val web_view = pane.web_view - web_view.setFontSmoothingType(FontSmoothingType.GRAY) - web_view.setOnKeyTyped(new EventHandler[KeyEvent] { - def handle(e: KeyEvent) { - if (e.isControlDown && e.getCharacter == "0") - web_view.setFontScale(1.0) - if (e.isControlDown && e.getCharacter == "+") - web_view.setFontScale(web_view.getFontScale * 1.1) - else if (e.isControlDown && e.getCharacter == "-") - web_view.setFontScale(web_view.getFontScale / 1.1) - } - }) - - setScene(new Scene(pane)) - pane - } - - def web_view: WebView = future.join.web_view - def web_engine: WebEngine = web_view.getEngine -} diff -r 58c9231c2937 -r 7b995cd6d5d4 src/Pure/GUI/jfx_gui.scala --- a/src/Pure/GUI/jfx_gui.scala Thu May 10 22:03:51 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,54 +0,0 @@ -/* Title: Pure/GUI/jfx_gui.scala - Author: Makarius - -Basic GUI tools (for Java FX). -*/ - -package isabelle - - -import java.io.{FileInputStream, BufferedInputStream} - -import javafx.application.{Platform => JFX_Platform} -import javafx.scene.text.{Font => JFX_Font} - - -object JFX_GUI -{ - /* evaluation within the Java FX application thread */ - - object Thread - { - def assert() = Predef.assert(JFX_Platform.isFxApplicationThread()) - def require() = Predef.require(JFX_Platform.isFxApplicationThread()) - - def later(body: => Unit) - { - if (JFX_Platform.isFxApplicationThread()) body - else JFX_Platform.runLater(new Runnable { def run = body }) - } - - def future[A](body: => A): Future[A] = - { - if (JFX_Platform.isFxApplicationThread()) Future.value(body) - else { - val promise = Future.promise[A] - later { promise.fulfill_result(Exn.capture(body)) } - promise - } - } - } - - - /* Isabelle fonts */ - - def install_fonts() - { - for (font <- Isabelle_System.fonts()) { - val stream = new BufferedInputStream(new FileInputStream(font.file)) - try { JFX_Font.loadFont(stream, 1.0) } - finally { stream.close } - } - } - -} diff -r 58c9231c2937 -r 7b995cd6d5d4 src/Pure/ROOT.scala --- a/src/Pure/ROOT.scala Thu May 10 22:03:51 2018 +0100 +++ b/src/Pure/ROOT.scala Fri May 11 11:42:23 2018 +0200 @@ -25,3 +25,4 @@ type UUID = java.util.UUID def UUID(): UUID = java.util.UUID.randomUUID() } + diff -r 58c9231c2937 -r 7b995cd6d5d4 src/Pure/build-jars --- a/src/Pure/build-jars Thu May 10 22:03:51 2018 +0100 +++ b/src/Pure/build-jars Fri May 11 11:42:23 2018 +0200 @@ -37,8 +37,6 @@ GUI/color_value.scala GUI/gui.scala GUI/gui_thread.scala - GUI/html5_panel.scala - GUI/jfx_gui.scala GUI/popup.scala GUI/wrap_panel.scala General/antiquote.scala