isabelle: src/Tools/jEdit/src/jedit/html_panel.scala@9dfcde68b383 (annotated)

36760 b82a698ef6c9 tuned headers; wenzelm parents: 36735 diff changeset	1	/* Title: Tools/jEdit/src/jedit/html_panel.scala
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
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	12	import java.io.StringReader
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	13	import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	14	import java.awt.event.MouseEvent
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	15
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	16	import javax.swing.{JButton, JPanel, JScrollPane}
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
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	40	class HTML_Panel(
36992 485c5e478ab6 tuned; wenzelm parents: 36991 diff changeset	41	system: Isabelle_System,
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	42	initial_font_size: Int,
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	43	handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	44	{
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	45	// global logging
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	46	Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	47
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	48
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	49	/* Lobo setup */
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	50
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	51	// 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	52	val screen_resolution =
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	53	if (GraphicsEnvironment.isHeadless()) 72
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	54	else Toolkit.getDefaultToolkit().getScreenResolution()
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	55
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	56	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	57	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	58
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	59
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	60	private val ucontext = new SimpleUserAgentContext
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	61	private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	62	{
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	63	private def handle(event: HTML_Panel.Event): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	64	if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	65	else false
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	66
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	67	override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	68	handle(HTML_Panel.Context_Menu(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	69	override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	70	handle(HTML_Panel.Mouse_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	71	override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	72	handle(HTML_Panel.Double_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	73	override def onMouseOver(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	74	{ handle(HTML_Panel.Mouse_Over(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	75	override def onMouseOut(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	76	{ handle(HTML_Panel.Mouse_Out(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	77	}
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	78
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	79	private val builder = new DocumentBuilderImpl(ucontext, rcontext)
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
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	82	/* document template with style sheets */
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	83
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	84	private val template_head =
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	85	"""<?xml version="1.0" encoding="utf-8"?>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	86	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	87	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	88	<html xmlns="http://www.w3.org/1999/xhtml">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	89	<head>
34770 0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	90	<style media="all" type="text/css">
0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	91	""" +
36992 485c5e478ab6 tuned; wenzelm parents: 36991 diff changeset	92	system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	93	system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n"
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	94
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	95	private val template_tail =
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	96	"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	97	</style>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	98	</head>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	99	<body/>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	100	</html>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	101	"""
37015 39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	102
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	103	private def template(font_size: Int): String =
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	104	template_head +
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	105	"body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	106	template_tail
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	107
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	108
39207774a9b7 read style sheets only once; wenzelm parents: 37014 diff changeset	109	/* physical document */
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	110
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	111	private class Doc
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	112	{
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	113	private var current_font_size: Int = 0
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	114	private var current_font_metrics: FontMetrics = null
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	115	private var current_body: List[XML.Tree] = Nil
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	116	private var current_DOM: org.w3c.dom.Document = null
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	117
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	118	def resize(font_size: Int)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	119	{
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	120	if (font_size != current_font_size \|\| current_font_metrics == null) {
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	121	Swing_Thread.now {
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	122	current_font_size = font_size
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	123	current_font_metrics =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	124	getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	125	}
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	126	current_DOM =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	127	builder.parse(
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	128	new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	129	refresh()
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	130	}
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	131	}
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	132
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	133	def refresh() { render(current_body) }
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	134
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	135	def render(body: List[XML.Tree])
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	136	{
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	137	current_body = body
36995 9421452afc29 determine margin just before rendering -- proper reformatting when updating; wenzelm parents: 36993 diff changeset	138	val margin = (getWidth() / (current_font_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	139	val html_body =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	140	current_body.flatMap(div =>
36995 9421452afc29 determine margin just before rendering -- proper reformatting when updating; wenzelm parents: 36993 diff changeset	141	Pretty.formatted(List(div), margin,
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	142	Pretty.font_metric(current_font_metrics))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	143	.map(t => XML.elem(HTML.PRE, HTML.spans(t))))
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	144
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	145	val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
37016 9dfcde68b383 mutate displayed document synchronously in Swing thread, for improved robustness; wenzelm parents: 37015 diff changeset	146	Swing_Thread.now {
9dfcde68b383 mutate displayed document synchronously in Swing thread, for improved robustness; wenzelm parents: 37015 diff changeset	147	current_DOM.removeChild(current_DOM.getLastChild())
9dfcde68b383 mutate displayed document synchronously in Swing thread, for improved robustness; wenzelm parents: 37015 diff changeset	148	current_DOM.appendChild(node)
9dfcde68b383 mutate displayed document synchronously in Swing thread, for improved robustness; wenzelm parents: 37015 diff changeset	149	setDocument(current_DOM, rcontext)
9dfcde68b383 mutate displayed document synchronously in Swing thread, for improved robustness; wenzelm parents: 37015 diff changeset	150	}
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	151	}
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	152
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	153	resize(initial_font_size)
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	154	}
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	155
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	156
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	157	/* main actor and method wrappers */
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	158
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	159	private case class Resize(font_size: Int)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	160	private case class Render(body: List[XML.Tree])
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	161	private case object Refresh
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	162
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	163	private val main_actor = actor {
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	164	var doc = new Doc
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	165	loop {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	166	react {
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	167	case Resize(font_size) => doc.resize(font_size)
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	168	case Refresh => doc.refresh()
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	169	case Render(body) => doc.render(body)
34769 826525fc5285 more precise messages; wenzelm parents: 34766 diff changeset	170	case bad => System.err.println("main_actor: ignoring bad message " + bad)
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	171	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	172	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	173	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	174
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	175	def resize(font_size: Int) { main_actor ! Resize(font_size) }
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36995 diff changeset	176	def refresh() { main_actor ! Refresh }
36993 b7cce32953f0 more systematic treatment of physical document wrt. font size etc.; wenzelm parents: 36992 diff changeset	177	def render(body: List[XML.Tree]) { main_actor ! Render(body) }
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	178	}

author	wenzelm
	Thu, 20 May 2010 21:10:03 +0200
changeset 37016	9dfcde68b383
parent 37015	39207774a9b7
child 37034	9640f6546179
permissions	-rw-r--r--