isabelle: src/Tools/jEdit/src/html_panel.scala@e1a09c2a6248 (annotated)

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 b82a698ef6c9 tuned headers; wenzelm parents: 36735 diff changeset	2	Author: Makarius
b82a698ef6c9 tuned headers; wenzelm parents: 36735 diff changeset	3
b82a698ef6c9 tuned headers; wenzelm parents: 36735 diff changeset	4	HTML panel based on Lobo/Cobra.
b82a698ef6c9 tuned headers; wenzelm parents: 36735 diff changeset	5	*/
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	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 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	8
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	9
36015 6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	10	import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	11
43520 cec9b95fa35d explicit import java.lang.System to prevent odd scope problems; wenzelm parents: 43455 diff changeset	12	import java.lang.System
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	13	import java.io.StringReader
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	14	import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	15	import java.awt.event.MouseEvent
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	16
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	17	import java.util.logging.{Logger, Level}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	18
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	19	import org.w3c.dom.html2.HTMLElement
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	20
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	21	import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	22	import org.lobobrowser.html.gui.HtmlPanel
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	23	import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	24	import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	25
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	26	import scala.actors.Actor._
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	27
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	28
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	29	object HTML_Panel
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	30	{
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	31	sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	32	case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	33	case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	34	case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	35	case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	36	case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	37	}
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	38
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	39
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	40	class HTML_Panel(
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	41	system: Isabelle_System,
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	42	initial_font_family: String,
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	43	initial_font_size: Int)
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	44	extends HtmlPanel
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	45	{
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	46	/ 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	47
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	48	/* 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	49
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	50	Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	51
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	52
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	53	/* 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	54
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	55	val screen_resolution =
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	56	if (GraphicsEnvironment.isHeadless()) 72
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	57	else Toolkit.getDefaultToolkit().getScreenResolution()
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	58
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	59	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	60	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	61
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	62
37036 49559c4e85f9 HTML_Panel.handler as overridable method; wenzelm parents: 37034 diff changeset	63	/* contexts and event handling */
49559c4e85f9 HTML_Panel.handler as overridable method; wenzelm parents: 37034 diff changeset	64
43442 e1fff67b23ac tuned -- Map.empty serves as partial function; wenzelm parents: 43282 diff changeset	65	protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Map.empty
37036 49559c4e85f9 HTML_Panel.handler as overridable method; wenzelm parents: 37034 diff changeset	66
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	67	private val ucontext = new SimpleUserAgentContext
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	68	private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
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	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	71	if (handler.isDefinedAt(event)) { handler(event); false }
9901f877eeb7 invert event propagation flag -- in lobobrowser api, true means re-propagate krauss parents: 39740 diff changeset	72	else true
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	73
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	74	override def onContextMenu(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.Context_Menu(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	76	override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	77	handle(HTML_Panel.Mouse_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	78	override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	79	handle(HTML_Panel.Double_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	80	override def onMouseOver(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	81	{ handle(HTML_Panel.Mouse_Over(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	82	override def onMouseOut(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	83	{ handle(HTML_Panel.Mouse_Out(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	84	}
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	85
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	86	private val builder = new DocumentBuilderImpl(ucontext, rcontext)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	87
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	88
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	89	/* document template with style sheets */
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	90
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	91	private val template_head =
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	92	"""<?xml version="1.0" encoding="utf-8"?>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	93	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	94	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	95	<html xmlns="http://www.w3.org/1999/xhtml">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	96	<head>
34770 0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	97	<style media="all" type="text/css">
0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	98	""" +
43606 e1a09c2a6248 prefer Isabelle path algebra; wenzelm parents: 43551 diff changeset	99	system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	100
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	101	private val template_tail =
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	102	"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	103	</style>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	104	</head>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	105	<body/>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	106	</html>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	107	"""
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	108
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	109	private def template(font_family: String, font_size: Int): String =
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	110	template_head +
37202 382a56c9f295 tuned; wenzelm parents: 37164 diff changeset	111	"body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	112	template_tail
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	113
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	114
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	115	/ 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	116
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	117	/* 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	118
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	119	private case class Resize(font_family: String, font_size: Int)
39590 2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	120	private case class Render_Document(text: String)
38573 d163f0f28e8c tuned signatures; wenzelm parents: 38444 diff changeset	121	private case class Render(body: XML.Body)
39740 0294948ba962 basic support for message popups via HTML_Panel; wenzelm parents: 39590 diff changeset	122	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	123	private case object Refresh
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	124
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	125	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	126
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	127	/* 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	128
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	129	var current_font_metrics: FontMetrics = null
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	130	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	131	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	132	var current_margin: Int = 0
38573 d163f0f28e8c tuned signatures; wenzelm parents: 38444 diff changeset	133	var current_body: XML.Body = Nil
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	134
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	135	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	136	{
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	137	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	138	val (font_metrics, margin) =
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	139	Swing_Thread.now {
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	140	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	141	(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	142	}
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	143	if (current_font_metrics == null \|\|
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	144	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	145	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	146	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	147	{
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	148	current_font_metrics = font_metrics
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	149	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	150	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	151	current_margin = margin
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	152	refresh()
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	153	}
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	154	}
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	155
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	156	def refresh() { render(current_body) }
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	157
39590 2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	158	def render_document(text: String)
2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	159	{
2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	160	val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	161	Swing_Thread.later { setDocument(doc, rcontext) }
2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	162	}
2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	163
38573 d163f0f28e8c tuned signatures; wenzelm parents: 38444 diff changeset	164	def render(body: XML.Body)
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	165	{
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	166	current_body = body
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	167	val html_body =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	168	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	169	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	170	.map(t =>
43551 07a9cbf2376f clarified Markup.CLASS vs. HTML.CLASS; wenzelm parents: 43520 diff changeset	171	XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))),
43455 4b4b93672f15 some unicode chars for special control symbols; wenzelm parents: 43442 diff changeset	172	HTML.spans(system.symbols, 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	173	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	174	builder.parse(
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	175	new InputSourceImpl(
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	176	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	177	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	178	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	179	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	180	}
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	181
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	182
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	183	/* main loop */
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	184
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	185	resize(initial_font_family, initial_font_size)
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	186
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	187	loop {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	188	react {
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	189	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	190	case Refresh => refresh()
39590 2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	191	case Render_Document(text) => render_document(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	192	case Render(body) => render(body)
39740 0294948ba962 basic support for message popups via HTML_Panel; wenzelm parents: 39590 diff changeset	193	case Render_Sync(body) => render(body); reply(())
34769 826525fc5285 more precise messages; wenzelm parents: 34766 diff changeset	194	case bad => System.err.println("main_actor: ignoring bad message " + bad)
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	195	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	196	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	197	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	198
37034 9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	199
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; wenzelm parents: 37016 diff changeset	200	/* 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	201
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37069 diff changeset	202	def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	203	def refresh() { main_actor ! Refresh }
39590 2258769f112f basic support for full document rendering; wenzelm parents: 38573 diff changeset	204	def render_document(text: String) { main_actor ! Render_Document(text) }
38573 d163f0f28e8c tuned signatures; wenzelm parents: 38444 diff changeset	205	def render(body: XML.Body) { main_actor ! Render(body) }
39740 0294948ba962 basic support for message popups via HTML_Panel; wenzelm parents: 39590 diff changeset	206	def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	207	}

author	wenzelm
	Thu, 30 Jun 2011 14:55:01 +0200
changeset 43606	e1a09c2a6248
parent 43551	07a9cbf2376f
child 43661	39fdbd814c7f
permissions	-rw-r--r--