|
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 } |