4 import java.awt.BorderLayout |
4 import java.awt.BorderLayout |
5 import javax.swing.{ JButton, JPanel, JScrollPane } |
5 import javax.swing.{ JButton, JPanel, JScrollPane } |
6 |
6 |
7 import isabelle.IsabelleSystem.getenv |
7 import isabelle.IsabelleSystem.getenv |
8 |
8 |
9 import org.w3c.dom.Document |
|
10 |
|
11 import org.xhtmlrenderer.simple.XHTMLPanel |
9 import org.xhtmlrenderer.simple.XHTMLPanel |
12 import org.xhtmlrenderer.context.AWTFontResolver |
10 import org.xhtmlrenderer.context.AWTFontResolver |
13 |
11 |
14 import org.gjt.sp.jedit.View |
12 import org.gjt.sp.jedit.View |
15 |
13 |
16 class StateViewDockable(view : View, position : String) extends JPanel { |
14 class StateViewDockable(view : View, position : String) extends JPanel { |
17 { |
15 val panel = new XHTMLPanel(new UserAgent()) |
18 val panel = new XHTMLPanel(new UserAgent()) |
16 setLayout(new BorderLayout) |
19 setLayout(new BorderLayout) |
|
20 |
17 |
21 //Copy-paste-support |
18 //Copy-paste-support |
22 val cp = new SelectionActions |
19 private val cp = new SelectionActions |
23 cp.install(panel) |
20 cp.install(panel) |
24 |
21 |
25 add(new JScrollPane(panel), BorderLayout.CENTER) |
22 add(new JScrollPane(panel), BorderLayout.CENTER) |
26 |
23 |
27 val fontResolver = |
24 private val fontResolver = |
28 panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
25 panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
|
26 if (Plugin.plugin.viewFont != null) |
|
27 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
|
28 |
|
29 Plugin.plugin.viewFontChanged.add(font => { |
29 if (Plugin.plugin.viewFont != null) |
30 if (Plugin.plugin.viewFont != null) |
30 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
31 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
31 |
32 |
32 Plugin.plugin.viewFontChanged.add(font => { |
33 panel.relayout() |
33 if (Plugin.plugin.viewFont != null) |
34 }) |
34 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
35 |
35 |
|
36 panel.relayout() |
|
37 }) |
|
38 |
|
39 Plugin.plugin.stateUpdate.add(state => { |
|
40 if (state == null) |
|
41 panel.setDocument(null : Document) |
|
42 else |
|
43 panel.setDocument(state.results_xml, UserAgent.baseURL) |
|
44 }) |
|
45 } |
|
46 } |
36 } |