| author | wenzelm |
| Fri, 07 May 2010 22:00:23 +0200 | |
| changeset 36735 | 42b7f881f5fc |
| parent 36015 | 6111de7c916a |
| child 36760 | b82a698ef6c9 |
| permissions | -rw-r--r-- |
| 34765 | 1 |
/* |
2 |
* HTML panel based on Lobo/Cobra |
|
3 |
* |
|
4 |
* @author Makarius |
|
5 |
*/ |
|
6 |
||
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34823
diff
changeset
|
7 |
package isabelle.jedit |
| 34765 | 8 |
|
9 |
||
| 36015 | 10 |
import isabelle._ |
11 |
||
| 34765 | 12 |
import java.io.StringReader |
13 |
import java.awt.{BorderLayout, Dimension}
|
|
| 34775 | 14 |
import java.awt.event.MouseEvent |
15 |
||
| 34765 | 16 |
import javax.swing.{JButton, JPanel, JScrollPane}
|
17 |
import java.util.logging.{Logger, Level}
|
|
18 |
||
| 34775 | 19 |
import org.w3c.dom.html2.HTMLElement |
| 34765 | 20 |
|
21 |
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
|
|
22 |
import org.lobobrowser.html.gui.HtmlPanel |
|
23 |
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
|
|
24 |
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
|
|
25 |
||
26 |
import scala.io.Source |
|
27 |
import scala.actors.Actor._ |
|
28 |
||
29 |
||
| 34775 | 30 |
object HTML_Panel |
31 |
{
|
|
32 |
sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
|
|
33 |
case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event |
|
34 |
case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event |
|
35 |
case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event |
|
36 |
case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event |
|
37 |
case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event |
|
38 |
} |
|
39 |
||
40 |
||
41 |
class HTML_Panel( |
|
42 |
sys: Isabelle_System, |
|
43 |
initial_font_size: Int, |
|
44 |
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel |
|
| 34765 | 45 |
{
|
46 |
// global logging |
|
47 |
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
|
|
48 |
||
49 |
||
50 |
/* document template */ |
|
51 |
||
52 |
private def try_file(name: String): String = |
|
53 |
{
|
|
54 |
val file = sys.platform_file(name) |
|
| 34776 | 55 |
if (file.isFile) Source.fromFile(file).mkString else "" |
| 34765 | 56 |
} |
57 |
||
58 |
private def template(font_size: Int): String = |
|
59 |
"""<?xml version="1.0" encoding="utf-8"?> |
|
60 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
|
61 |
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
62 |
<html xmlns="http://www.w3.org/1999/xhtml"> |
|
63 |
<head> |
|
| 34770 | 64 |
<style media="all" type="text/css"> |
65 |
""" + |
|
| 34765 | 66 |
try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
|
67 |
try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
|
|
| 34770 | 68 |
"body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
|
| 34765 | 69 |
""" |
70 |
</style> |
|
71 |
</head> |
|
72 |
<body/> |
|
73 |
</html> |
|
74 |
""" |
|
75 |
||
76 |
||
77 |
/* actor with local state */ |
|
78 |
||
79 |
private val ucontext = new SimpleUserAgentContext |
|
| 34775 | 80 |
|
| 34765 | 81 |
private val rcontext = new SimpleHtmlRendererContext(this, ucontext) |
| 34775 | 82 |
{
|
83 |
private def handle(event: HTML_Panel.Event): Boolean = |
|
84 |
if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
|
|
85 |
else false |
|
86 |
||
87 |
override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = |
|
88 |
handle(HTML_Panel.Context_Menu(elem, event)) |
|
89 |
override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean = |
|
90 |
handle(HTML_Panel.Mouse_Click(elem, event)) |
|
91 |
override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean = |
|
92 |
handle(HTML_Panel.Double_Click(elem, event)) |
|
93 |
override def onMouseOver(elem: HTMLElement, event: MouseEvent) |
|
94 |
{ handle(HTML_Panel.Mouse_Over(elem, event)) }
|
|
95 |
override def onMouseOut(elem: HTMLElement, event: MouseEvent) |
|
96 |
{ handle(HTML_Panel.Mouse_Out(elem, event)) }
|
|
97 |
} |
|
98 |
||
| 34765 | 99 |
private val builder = new DocumentBuilderImpl(ucontext, rcontext) |
100 |
||
101 |
private case class Init(font_size: Int) |
|
102 |
private case class Render(body: List[XML.Tree]) |
|
103 |
||
104 |
private val main_actor = actor {
|
|
| 34791 | 105 |
// crude double buffering |
| 34823 | 106 |
var doc1: org.w3c.dom.Document = null |
107 |
var doc2: org.w3c.dom.Document = null |
|
| 34765 | 108 |
|
109 |
loop {
|
|
110 |
react {
|
|
111 |
case Init(font_size) => |
|
112 |
val src = template(font_size) |
|
| 34766 | 113 |
def parse() = |
114 |
builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost")) |
|
| 34765 | 115 |
doc1 = parse() |
116 |
doc2 = parse() |
|
117 |
Swing_Thread.now { setDocument(doc1, rcontext) }
|
|
118 |
||
119 |
case Render(body) => |
|
120 |
val doc = doc2 |
|
|
36735
42b7f881f5fc
output symbolic pretty printing markup and format in the front end;
wenzelm
parents:
36015
diff
changeset
|
121 |
val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t))) |
|
42b7f881f5fc
output symbolic pretty printing markup and format in the front end;
wenzelm
parents:
36015
diff
changeset
|
122 |
val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body)) |
| 34765 | 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 |
} |