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