--- 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
-}
--- 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 }
- }
- }
-
-}
--- 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()
}
+
--- 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