removed unused Java FX modules (it will be unbundled from JDK eventually);
authorwenzelm
Fri May 11 11:42:23 2018 +0200 (2018-05-11)
changeset 681447b995cd6d5d4
parent 68143 58c9231c2937
child 68145 edacd2a050be
removed unused Java FX modules (it will be unbundled from JDK eventually);
src/Pure/GUI/html5_panel.scala
src/Pure/GUI/jfx_gui.scala
src/Pure/ROOT.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/GUI/html5_panel.scala	Thu May 10 22:03:51 2018 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,78 +0,0 @@
     1.4 -/*  Title:      Pure/GUI/html5_panel.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -HTML5 panel based on Java FX WebView.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -import javafx.scene.Scene
    1.14 -import javafx.scene.web.{WebView, WebEngine}
    1.15 -import javafx.scene.input.KeyEvent
    1.16 -import javafx.scene.text.FontSmoothingType
    1.17 -import javafx.scene.layout.{HBox, VBox, Priority}
    1.18 -import javafx.geometry.{HPos, VPos, Insets}
    1.19 -import javafx.event.EventHandler
    1.20 -
    1.21 -
    1.22 -// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
    1.23 -// and http://hg.netbeans.org/jet-main/rev/a88434cec458
    1.24 -private class Web_View_Workaround extends javafx.scene.layout.Pane
    1.25 -{
    1.26 -  VBox.setVgrow(this, Priority.ALWAYS)
    1.27 -  HBox.setHgrow(this, Priority.ALWAYS)
    1.28 -
    1.29 -  setMaxWidth(java.lang.Double.MAX_VALUE)
    1.30 -  setMaxHeight(java.lang.Double.MAX_VALUE)
    1.31 -
    1.32 -  val web_view = new WebView
    1.33 -  web_view.setMinSize(500, 400)
    1.34 -  web_view.setPrefSize(500, 400)
    1.35 -
    1.36 -  getChildren().add(web_view)
    1.37 -
    1.38 -  override protected def layoutChildren()
    1.39 -  {
    1.40 -    val managed = getManagedChildren()
    1.41 -    val width = getWidth()
    1.42 -    val height = getHeight()
    1.43 -    val top = getInsets().getTop()
    1.44 -    val right = getInsets().getRight()
    1.45 -    val left = getInsets().getLeft()
    1.46 -    val bottom = getInsets().getBottom()
    1.47 -
    1.48 -    for (i <- 0 until managed.size)
    1.49 -      layoutInArea(managed.get(i), left, top,
    1.50 -        width - left - right, height - top - bottom,
    1.51 -        0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
    1.52 -  }
    1.53 -}
    1.54 -
    1.55 -
    1.56 -class HTML5_Panel extends javafx.embed.swing.JFXPanel
    1.57 -{
    1.58 -  private val future =
    1.59 -    JFX_GUI.Thread.future {
    1.60 -      val pane = new Web_View_Workaround
    1.61 -
    1.62 -      val web_view = pane.web_view
    1.63 -      web_view.setFontSmoothingType(FontSmoothingType.GRAY)
    1.64 -      web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
    1.65 -        def handle(e: KeyEvent) {
    1.66 -          if (e.isControlDown && e.getCharacter == "0")
    1.67 -            web_view.setFontScale(1.0)
    1.68 -          if (e.isControlDown && e.getCharacter == "+")
    1.69 -            web_view.setFontScale(web_view.getFontScale * 1.1)
    1.70 -          else if (e.isControlDown && e.getCharacter == "-")
    1.71 -            web_view.setFontScale(web_view.getFontScale / 1.1)
    1.72 -        }
    1.73 -      })
    1.74 -
    1.75 -      setScene(new Scene(pane))
    1.76 -      pane
    1.77 -    }
    1.78 -
    1.79 -  def web_view: WebView = future.join.web_view
    1.80 -  def web_engine: WebEngine = web_view.getEngine
    1.81 -}
     2.1 --- a/src/Pure/GUI/jfx_gui.scala	Thu May 10 22:03:51 2018 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,54 +0,0 @@
     2.4 -/*  Title:      Pure/GUI/jfx_gui.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Basic GUI tools (for Java FX).
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -import java.io.{FileInputStream, BufferedInputStream}
    2.14 -
    2.15 -import javafx.application.{Platform => JFX_Platform}
    2.16 -import javafx.scene.text.{Font => JFX_Font}
    2.17 -
    2.18 -
    2.19 -object JFX_GUI
    2.20 -{
    2.21 -  /* evaluation within the Java FX application thread */
    2.22 -
    2.23 -  object Thread
    2.24 -  {
    2.25 -    def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
    2.26 -    def require() = Predef.require(JFX_Platform.isFxApplicationThread())
    2.27 -
    2.28 -    def later(body: => Unit)
    2.29 -    {
    2.30 -      if (JFX_Platform.isFxApplicationThread()) body
    2.31 -      else JFX_Platform.runLater(new Runnable { def run = body })
    2.32 -    }
    2.33 -
    2.34 -    def future[A](body: => A): Future[A] =
    2.35 -    {
    2.36 -      if (JFX_Platform.isFxApplicationThread()) Future.value(body)
    2.37 -      else {
    2.38 -        val promise = Future.promise[A]
    2.39 -        later { promise.fulfill_result(Exn.capture(body)) }
    2.40 -        promise
    2.41 -      }
    2.42 -    }
    2.43 -  }
    2.44 -
    2.45 -
    2.46 -  /* Isabelle fonts */
    2.47 -
    2.48 -  def install_fonts()
    2.49 -  {
    2.50 -    for (font <- Isabelle_System.fonts()) {
    2.51 -      val stream = new BufferedInputStream(new FileInputStream(font.file))
    2.52 -      try { JFX_Font.loadFont(stream, 1.0) }
    2.53 -      finally { stream.close }
    2.54 -    }
    2.55 -  }
    2.56 -
    2.57 -}
     3.1 --- a/src/Pure/ROOT.scala	Thu May 10 22:03:51 2018 +0100
     3.2 +++ b/src/Pure/ROOT.scala	Fri May 11 11:42:23 2018 +0200
     3.3 @@ -25,3 +25,4 @@
     3.4    type UUID = java.util.UUID
     3.5    def UUID(): UUID = java.util.UUID.randomUUID()
     3.6  }
     3.7 +
     4.1 --- a/src/Pure/build-jars	Thu May 10 22:03:51 2018 +0100
     4.2 +++ b/src/Pure/build-jars	Fri May 11 11:42:23 2018 +0200
     4.3 @@ -37,8 +37,6 @@
     4.4    GUI/color_value.scala
     4.5    GUI/gui.scala
     4.6    GUI/gui_thread.scala
     4.7 -  GUI/html5_panel.scala
     4.8 -  GUI/jfx_gui.scala
     4.9    GUI/popup.scala
    4.10    GUI/wrap_panel.scala
    4.11    General/antiquote.scala