author | wenzelm |
Mon, 28 Nov 2011 22:05:32 +0100 | |
changeset 45666 | d83797ef0d2d |
parent 45099 | 67740480cf39 |
child 48550 | 97592027a2a8 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
42976
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/html_panel.scala |
36760 | 2 |
Author: Makarius |
3 |
||
4 |
HTML panel based on Lobo/Cobra. |
|
5 |
*/ |
|
34765 | 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 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43455
diff
changeset
|
12 |
import java.lang.System |
34765 | 13 |
import java.io.StringReader |
37164 | 14 |
import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics} |
34775 | 15 |
import java.awt.event.MouseEvent |
16 |
||
34765 | 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.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 |
||
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43606
diff
changeset
|
40 |
class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel |
34765 | 41 |
{ |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
42 |
/** Lobo setup **/ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
43 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
44 |
/* global logging */ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
45 |
|
34765 | 46 |
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) |
47 |
||
48 |
||
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
49 |
/* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */ |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
50 |
|
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
51 |
val screen_resolution = |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
52 |
if (GraphicsEnvironment.isHeadless()) 72 |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
53 |
else Toolkit.getDefaultToolkit().getScreenResolution() |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
54 |
|
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
55 |
def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
56 |
def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96 |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
57 |
|
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
58 |
|
37036 | 59 |
/* contexts and event handling */ |
60 |
||
43442 | 61 |
protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Map.empty |
37036 | 62 |
|
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
63 |
private val ucontext = new SimpleUserAgentContext |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
64 |
private val rcontext = new SimpleHtmlRendererContext(this, ucontext) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
65 |
{ |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
66 |
private def handle(event: HTML_Panel.Event): Boolean = |
42976
9901f877eeb7
invert event propagation flag -- in lobobrowser api, true means re-propagate
krauss
parents:
39740
diff
changeset
|
67 |
if (handler.isDefinedAt(event)) { handler(event); false } |
9901f877eeb7
invert event propagation flag -- in lobobrowser api, true means re-propagate
krauss
parents:
39740
diff
changeset
|
68 |
else true |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
69 |
|
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
70 |
override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
71 |
handle(HTML_Panel.Context_Menu(elem, event)) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
72 |
override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean = |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
73 |
handle(HTML_Panel.Mouse_Click(elem, event)) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
74 |
override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean = |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
75 |
handle(HTML_Panel.Double_Click(elem, event)) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
76 |
override def onMouseOver(elem: HTMLElement, event: MouseEvent) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
77 |
{ handle(HTML_Panel.Mouse_Over(elem, event)) } |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
78 |
override def onMouseOut(elem: HTMLElement, event: MouseEvent) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
79 |
{ handle(HTML_Panel.Mouse_Out(elem, event)) } |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
80 |
} |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
81 |
|
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
82 |
private val builder = new DocumentBuilderImpl(ucontext, rcontext) |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
83 |
|
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
84 |
|
37015 | 85 |
/* document template with style sheets */ |
34765 | 86 |
|
37015 | 87 |
private val template_head = |
34765 | 88 |
"""<?xml version="1.0" encoding="utf-8"?> |
89 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
|
90 |
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
91 |
<html xmlns="http://www.w3.org/1999/xhtml"> |
|
92 |
<head> |
|
34770 | 93 |
<style media="all" type="text/css"> |
94 |
""" + |
|
43669 | 95 |
Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS"))) |
37015 | 96 |
|
97 |
private val template_tail = |
|
34765 | 98 |
""" |
99 |
</style> |
|
100 |
</head> |
|
101 |
<body/> |
|
102 |
</html> |
|
103 |
""" |
|
37015 | 104 |
|
37164 | 105 |
private def template(font_family: String, font_size: Int): String = |
37015 | 106 |
template_head + |
37202 | 107 |
"body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" + |
37015 | 108 |
template_tail |
109 |
||
110 |
||
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
111 |
/** main actor **/ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
112 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
113 |
/* internal messages */ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
114 |
|
37164 | 115 |
private case class Resize(font_family: String, font_size: Int) |
45099 | 116 |
private case class Render_Document(url: String, text: String) |
38573 | 117 |
private case class Render(body: XML.Body) |
39740 | 118 |
private case class Render_Sync(body: XML.Body) |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
119 |
private case object Refresh |
34765 | 120 |
|
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
121 |
private val main_actor = actor { |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
122 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
123 |
/* internal state */ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
124 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
125 |
var current_font_metrics: FontMetrics = null |
37164 | 126 |
var current_font_family = "" |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
127 |
var current_font_size: Int = 0 |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
128 |
var current_margin: Int = 0 |
38573 | 129 |
var current_body: XML.Body = Nil |
34765 | 130 |
|
37164 | 131 |
def resize(font_family: String, font_size: Int) |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
132 |
{ |
37164 | 133 |
val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size))) |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
134 |
val (font_metrics, margin) = |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
135 |
Swing_Thread.now { |
37164 | 136 |
val metrics = getFontMetrics(font) |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
137 |
(metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20) |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
138 |
} |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
139 |
if (current_font_metrics == null || |
37164 | 140 |
current_font_family != font_family || |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
141 |
current_font_size != font_size || |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
142 |
current_margin != margin) |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
143 |
{ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
144 |
current_font_metrics = font_metrics |
37164 | 145 |
current_font_family = font_family |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
146 |
current_font_size = font_size |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
147 |
current_margin = margin |
37014 | 148 |
refresh() |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
149 |
} |
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36790
diff
changeset
|
150 |
} |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36790
diff
changeset
|
151 |
|
37014 | 152 |
def refresh() { render(current_body) } |
153 |
||
45099 | 154 |
def render_document(url: String, text: String) |
39590 | 155 |
{ |
45099 | 156 |
val doc = builder.parse(new InputSourceImpl(new StringReader(text), url)) |
39590 | 157 |
Swing_Thread.later { setDocument(doc, rcontext) } |
158 |
} |
|
159 |
||
38573 | 160 |
def render(body: XML.Body) |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
161 |
{ |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
162 |
current_body = body |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
163 |
val html_body = |
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
164 |
current_body.flatMap(div => |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
165 |
Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) |
38235
25d6f789618b
fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
wenzelm
parents:
37202
diff
changeset
|
166 |
.map(t => |
45666 | 167 |
XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))), |
168 |
HTML.spans(t, true)))) |
|
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
169 |
val doc = |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
170 |
builder.parse( |
37164 | 171 |
new InputSourceImpl( |
172 |
new StringReader(template(current_font_family, current_font_size)), "http://localhost")) |
|
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
173 |
doc.removeChild(doc.getLastChild()) |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
174 |
doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body))) |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
175 |
Swing_Thread.later { setDocument(doc, rcontext) } |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
176 |
} |
34775 | 177 |
|
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
178 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
179 |
/* main loop */ |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36992
diff
changeset
|
180 |
|
37164 | 181 |
resize(initial_font_family, initial_font_size) |
34775 | 182 |
|
34765 | 183 |
loop { |
184 |
react { |
|
37164 | 185 |
case Resize(font_family, font_size) => resize(font_family, font_size) |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
186 |
case Refresh => refresh() |
45099 | 187 |
case Render_Document(url, text) => render_document(url, text) |
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
188 |
case Render(body) => render(body) |
39740 | 189 |
case Render_Sync(body) => render(body); reply(()) |
34769 | 190 |
case bad => System.err.println("main_actor: ignoring bad message " + bad) |
34765 | 191 |
} |
192 |
} |
|
193 |
} |
|
194 |
||
37034
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
195 |
|
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
196 |
/* external methods */ |
9640f6546179
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents:
37016
diff
changeset
|
197 |
|
37164 | 198 |
def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) } |
37014 | 199 |
def refresh() { main_actor ! Refresh } |
45099 | 200 |
def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) } |
38573 | 201 |
def render(body: XML.Body) { main_actor ! Render(body) } |
39740 | 202 |
def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) } |
34765 | 203 |
} |