1 /* |
|
2 * Dockable window with rendered state output |
|
3 * |
|
4 * @author Fabian Immler, TU Munich |
|
5 * @author Johannes Hölzl, TU Munich |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 import isabelle.XML |
|
11 |
|
12 import java.io.StringReader |
|
13 import java.awt.{BorderLayout, Dimension} |
|
14 |
|
15 import javax.swing.{JButton, JPanel, JScrollPane} |
|
16 |
|
17 import java.util.logging.{Logger, Level} |
|
18 |
|
19 import org.lobobrowser.html.parser._ |
|
20 import org.lobobrowser.html.test._ |
|
21 import org.lobobrowser.html.gui._ |
|
22 import org.lobobrowser.html._ |
|
23 import org.lobobrowser.html.style.CSSUtilities |
|
24 import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl} |
|
25 |
|
26 import org.gjt.sp.jedit.jEdit |
|
27 import org.gjt.sp.jedit.View |
|
28 import org.gjt.sp.jedit.gui.DockableWindowManager |
|
29 import org.gjt.sp.jedit.textarea.AntiAlias |
|
30 |
|
31 import scala.io.Source |
|
32 |
|
33 |
|
34 class StateViewDockable(view : View, position : String) extends JPanel { |
|
35 |
|
36 // outer panel |
|
37 if (position == DockableWindowManager.FLOATING) |
|
38 setPreferredSize(new Dimension(500, 250)) |
|
39 setLayout(new BorderLayout) |
|
40 |
|
41 |
|
42 // global logging |
|
43 |
|
44 Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) |
|
45 |
|
46 |
|
47 // document template with styles |
|
48 |
|
49 private def try_file(name: String): String = |
|
50 { |
|
51 val file = Isabelle.system.platform_file(name) |
|
52 if (file.exists) Source.fromFile(file).mkString else "" |
|
53 } |
|
54 |
|
55 |
|
56 // HTML panel |
|
57 |
|
58 val panel = new HtmlPanel |
|
59 val ucontext = new SimpleUserAgentContext |
|
60 val rcontext = new SimpleHtmlRendererContext(panel, ucontext) |
|
61 val doc = { |
|
62 val builder = new DocumentBuilderImpl(ucontext, rcontext) |
|
63 builder.parse(new InputSourceImpl(new StringReader( |
|
64 """<?xml version="1.0" encoding="utf-8"?> |
|
65 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
|
66 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
67 <html xmlns="http://www.w3.org/1999/xhtml"> |
|
68 <head> |
|
69 <style media="all" type="text/css"> |
|
70 """ + |
|
71 try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" + |
|
72 """ |
|
73 body { |
|
74 font-family: IsabelleText; |
|
75 font-size: 14pt; |
|
76 } |
|
77 """ + |
|
78 try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" + |
|
79 """ |
|
80 </style> |
|
81 </head> |
|
82 </html> |
|
83 """))) |
|
84 } |
|
85 |
|
86 val empty_body = XML.document_node(doc, XML.elem(HTML.BODY)) |
|
87 doc.appendChild(empty_body) |
|
88 |
|
89 panel.setDocument(doc, rcontext) |
|
90 add(panel, BorderLayout.CENTER) |
|
91 |
|
92 |
|
93 // register for state-view |
|
94 Isabelle.plugin.state_update += (cmd => { |
|
95 val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view |
|
96 |
|
97 Swing_Thread.later { |
|
98 val node = |
|
99 if (cmd == null) empty_body |
|
100 else { |
|
101 val xml = XML.elem(HTML.BODY, |
|
102 cmd.results(theory_view.current_document). |
|
103 map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))) |
|
104 XML.document_node(doc, xml) |
|
105 } |
|
106 doc.removeChild(doc.getLastChild()) |
|
107 doc.appendChild(node) |
|
108 panel.delayedRelayout(node.asInstanceOf[NodeImpl]) |
|
109 } |
|
110 }) |
|
111 } |
|