|
34765
|
1 |
/*
|
|
|
2 |
* HTML panel based on Lobo/Cobra
|
|
|
3 |
*
|
|
|
4 |
* @author Makarius
|
|
|
5 |
*/
|
|
|
6 |
|
|
|
7 |
package isabelle.proofdocument
|
|
|
8 |
|
|
|
9 |
|
|
|
10 |
import java.io.StringReader
|
|
|
11 |
import java.awt.{BorderLayout, Dimension}
|
|
34775
|
12 |
import java.awt.event.MouseEvent
|
|
|
13 |
|
|
34765
|
14 |
import javax.swing.{JButton, JPanel, JScrollPane}
|
|
|
15 |
import java.util.logging.{Logger, Level}
|
|
|
16 |
|
|
|
17 |
import org.w3c.dom.Document
|
|
34775
|
18 |
import org.w3c.dom.html2.HTMLElement
|
|
34765
|
19 |
|
|
|
20 |
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
|
|
|
21 |
import org.lobobrowser.html.gui.HtmlPanel
|
|
|
22 |
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
|
|
|
23 |
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
|
|
|
24 |
|
|
|
25 |
import scala.io.Source
|
|
|
26 |
import scala.actors.Actor._
|
|
|
27 |
|
|
|
28 |
|
|
34775
|
29 |
object HTML_Panel
|
|
|
30 |
{
|
|
|
31 |
sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
|
|
|
32 |
case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
|
|
|
33 |
case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
|
|
|
34 |
case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
|
|
|
35 |
case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
|
|
|
36 |
case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
|
|
|
37 |
}
|
|
|
38 |
|
|
|
39 |
|
|
|
40 |
class HTML_Panel(
|
|
|
41 |
sys: Isabelle_System,
|
|
|
42 |
initial_font_size: Int,
|
|
|
43 |
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
|
|
34765
|
44 |
{
|
|
|
45 |
// global logging
|
|
|
46 |
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
|
|
|
47 |
|
|
|
48 |
|
|
|
49 |
/* document template */
|
|
|
50 |
|
|
|
51 |
private def try_file(name: String): String =
|
|
|
52 |
{
|
|
|
53 |
val file = sys.platform_file(name)
|
|
34776
|
54 |
if (file.isFile) Source.fromFile(file).mkString else ""
|
|
34765
|
55 |
}
|
|
|
56 |
|
|
|
57 |
private def template(font_size: Int): String =
|
|
|
58 |
"""<?xml version="1.0" encoding="utf-8"?>
|
|
|
59 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
|
|
|
60 |
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
|
|
|
61 |
<html xmlns="http://www.w3.org/1999/xhtml">
|
|
|
62 |
<head>
|
|
34770
|
63 |
<style media="all" type="text/css">
|
|
|
64 |
""" +
|
|
34765
|
65 |
try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
|
|
|
66 |
try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
|
|
34770
|
67 |
"body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
|
|
34765
|
68 |
"""
|
|
|
69 |
</style>
|
|
|
70 |
</head>
|
|
|
71 |
<body/>
|
|
|
72 |
</html>
|
|
|
73 |
"""
|
|
|
74 |
|
|
|
75 |
|
|
|
76 |
/* actor with local state */
|
|
|
77 |
|
|
|
78 |
private val ucontext = new SimpleUserAgentContext
|
|
34775
|
79 |
|
|
34765
|
80 |
private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
|
|
34775
|
81 |
{
|
|
|
82 |
private def handle(event: HTML_Panel.Event): Boolean =
|
|
|
83 |
if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
|
|
|
84 |
else false
|
|
|
85 |
|
|
|
86 |
override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
|
|
|
87 |
handle(HTML_Panel.Context_Menu(elem, event))
|
|
|
88 |
override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
|
|
|
89 |
handle(HTML_Panel.Mouse_Click(elem, event))
|
|
|
90 |
override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
|
|
|
91 |
handle(HTML_Panel.Double_Click(elem, event))
|
|
|
92 |
override def onMouseOver(elem: HTMLElement, event: MouseEvent)
|
|
|
93 |
{ handle(HTML_Panel.Mouse_Over(elem, event)) }
|
|
|
94 |
override def onMouseOut(elem: HTMLElement, event: MouseEvent)
|
|
|
95 |
{ handle(HTML_Panel.Mouse_Out(elem, event)) }
|
|
|
96 |
}
|
|
|
97 |
|
|
34765
|
98 |
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
|
|
|
99 |
|
|
|
100 |
private case class Init(font_size: Int)
|
|
|
101 |
private case class Render(body: List[XML.Tree])
|
|
|
102 |
|
|
|
103 |
private val main_actor = actor {
|
|
34791
|
104 |
// crude double buffering
|
|
34765
|
105 |
var doc1: Document = null
|
|
|
106 |
var doc2: Document = null
|
|
|
107 |
|
|
|
108 |
loop {
|
|
|
109 |
react {
|
|
|
110 |
case Init(font_size) =>
|
|
|
111 |
val src = template(font_size)
|
|
34766
|
112 |
def parse() =
|
|
|
113 |
builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
|
|
34765
|
114 |
doc1 = parse()
|
|
|
115 |
doc2 = parse()
|
|
|
116 |
Swing_Thread.now { setDocument(doc1, rcontext) }
|
|
|
117 |
|
|
|
118 |
case Render(body) =>
|
|
|
119 |
val doc = doc2
|
|
|
120 |
val node =
|
|
|
121 |
XML.document_node(doc,
|
|
|
122 |
XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
|
|
|
123 |
doc.removeChild(doc.getLastChild())
|
|
|
124 |
doc.appendChild(node)
|
|
|
125 |
doc2 = doc1
|
|
|
126 |
doc1 = doc
|
|
|
127 |
Swing_Thread.now { setDocument(doc1, rcontext) }
|
|
|
128 |
|
|
34769
|
129 |
case bad => System.err.println("main_actor: ignoring bad message " + bad)
|
|
34765
|
130 |
}
|
|
|
131 |
}
|
|
|
132 |
}
|
|
|
133 |
|
|
|
134 |
main_actor ! Init(initial_font_size)
|
|
|
135 |
|
|
|
136 |
|
|
|
137 |
/* main method wrappers */
|
|
|
138 |
|
|
|
139 |
def init(font_size: Int) { main_actor ! Init(font_size) }
|
|
|
140 |
def render(body: List[XML.Tree]) { main_actor ! Render(body) }
|
|
|
141 |
}
|