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