src/Pure/System/html5_panel.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 49612 e6a53d203362
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm@49066
     1
/*  Title:      Pure/System/html5_panel.scala
wenzelm@49066
     2
    Author:     Makarius
wenzelm@49066
     3
wenzelm@49066
     4
HTML5 panel based on Java FX WebView.
wenzelm@49066
     5
*/
wenzelm@49066
     6
wenzelm@49066
     7
package isabelle
wenzelm@49066
     8
wenzelm@49066
     9
wenzelm@49066
    10
import javafx.scene.Scene
wenzelm@49066
    11
import javafx.scene.web.{WebView, WebEngine}
wenzelm@49066
    12
import javafx.scene.input.KeyEvent
wenzelm@49612
    13
import javafx.scene.text.FontSmoothingType
wenzelm@49066
    14
import javafx.scene.layout.{HBox, VBox, Priority}
wenzelm@49066
    15
import javafx.geometry.{HPos, VPos, Insets}
wenzelm@49066
    16
import javafx.event.EventHandler
wenzelm@49066
    17
wenzelm@49066
    18
wenzelm@49066
    19
// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
wenzelm@49066
    20
// and http://hg.netbeans.org/jet-main/rev/a88434cec458
wenzelm@49066
    21
private class Web_View_Workaround extends javafx.scene.layout.Pane
wenzelm@49066
    22
{
wenzelm@49066
    23
  VBox.setVgrow(this, Priority.ALWAYS)
wenzelm@49066
    24
  HBox.setHgrow(this, Priority.ALWAYS)
wenzelm@49066
    25
wenzelm@49066
    26
  setMaxWidth(java.lang.Double.MAX_VALUE)
wenzelm@49066
    27
  setMaxHeight(java.lang.Double.MAX_VALUE)
wenzelm@49066
    28
wenzelm@49066
    29
  val web_view = new WebView
wenzelm@49066
    30
  web_view.setMinSize(500, 400)
wenzelm@49066
    31
  web_view.setPrefSize(500, 400)
wenzelm@49066
    32
wenzelm@49066
    33
  getChildren().add(web_view)
wenzelm@49066
    34
wenzelm@49066
    35
  override protected def layoutChildren()
wenzelm@49066
    36
  {
wenzelm@49066
    37
    val managed = getManagedChildren()
wenzelm@49066
    38
    val width = getWidth()
wenzelm@49066
    39
    val height = getHeight()
wenzelm@49066
    40
    val top = getInsets().getTop()
wenzelm@49066
    41
    val right = getInsets().getRight()
wenzelm@49066
    42
    val left = getInsets().getLeft()
wenzelm@49066
    43
    val bottom = getInsets().getBottom()
wenzelm@49066
    44
wenzelm@49066
    45
    for (i <- 0 until managed.size)
wenzelm@49066
    46
      layoutInArea(managed.get(i), left, top,
wenzelm@49066
    47
        width - left - right, height - top - bottom,
wenzelm@49066
    48
        0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
wenzelm@49066
    49
  }
wenzelm@49066
    50
}
wenzelm@49066
    51
wenzelm@49066
    52
wenzelm@49612
    53
class HTML5_Panel extends javafx.embed.swing.JFXPanel
wenzelm@49066
    54
{
wenzelm@49066
    55
  private val future =
wenzelm@49066
    56
    JFX_Thread.future {
wenzelm@49066
    57
      val pane = new Web_View_Workaround
wenzelm@49066
    58
wenzelm@49066
    59
      val web_view = pane.web_view
wenzelm@49066
    60
      web_view.setFontSmoothingType(FontSmoothingType.GRAY)
wenzelm@49066
    61
      web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
wenzelm@49066
    62
        def handle(e: KeyEvent) {
wenzelm@49066
    63
          if (e.isControlDown && e.getCharacter == "0")
wenzelm@49066
    64
            web_view.setFontScale(1.0)
wenzelm@49066
    65
          if (e.isControlDown && e.getCharacter == "+")
wenzelm@49066
    66
            web_view.setFontScale(web_view.getFontScale * 1.1)
wenzelm@49066
    67
          else if (e.isControlDown && e.getCharacter == "-")
wenzelm@49066
    68
            web_view.setFontScale(web_view.getFontScale / 1.1)
wenzelm@49066
    69
        }
wenzelm@49066
    70
      })
wenzelm@49066
    71
wenzelm@49066
    72
      setScene(new Scene(pane))
wenzelm@49066
    73
      pane
wenzelm@49066
    74
    }
wenzelm@49066
    75
wenzelm@49066
    76
  def web_view: WebView = future.join.web_view
wenzelm@49066
    77
  def web_engine: WebEngine = web_view.getEngine
wenzelm@49066
    78
}