isabelle: src/Tools/jEdit/src/jedit/html_panel.scala@ed97e877ff2d (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.io.Source
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	27	import scala.actors.Actor._
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	28
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	29
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	30	object HTML_Panel
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	31	{
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	32	sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	33	case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	34	case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	35	case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	36	case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	37	case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
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
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	41	class HTML_Panel(
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	42	sys: Isabelle_System,
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	43	initial_font_size: Int,
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	44	handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	45	{
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	46	// global logging
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	47	Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	48
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	49
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	50	/* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	51
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
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	60	/* document template */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	61
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	62	private def try_file(name: String): String =
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	63	{
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	64	val file = sys.platform_file(name)
34776 01a9bfd64b87 tuned; wenzelm parents: 34775 diff changeset	65	if (file.isFile) Source.fromFile(file).mkString else ""
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	66	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	67
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	68	private def template(font_size: Int): String =
36790 c8deab866174 font size re-adjustment according to Lobo internals; wenzelm parents: 36760 diff changeset	69	{
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	70	"""<?xml version="1.0" encoding="utf-8"?>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	71	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	72	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	73	<html xmlns="http://www.w3.org/1999/xhtml">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	74	<head>
34770 0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	75	<style media="all" type="text/css">
0c630c52fc74 prefer options from running application; wenzelm parents: 34769 diff changeset	76	""" +
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	77	try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	78	try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	79	"body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	80	"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	81	</style>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	82	</head>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	83	<body/>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	84	</html>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	85	"""
36790 c8deab866174 font size re-adjustment according to Lobo internals; wenzelm parents: 36760 diff changeset	86	}
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	87
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	88	def font_metrics(font_size: Int): FontMetrics =
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	89	Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	90
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	91	def panel_width(font_size: Int): Int =
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	92	Swing_Thread.now {
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	93	(getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	94	}
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	95
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	96
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	97	/* actor with local state */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	98
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	99	private val ucontext = new SimpleUserAgentContext
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	100
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	101	private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
34775 49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	102	{
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	103	private def handle(event: HTML_Panel.Event): Boolean =
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	104	if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	105	else false
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	106
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	107	override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	108	handle(HTML_Panel.Context_Menu(elem, event))
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	109	override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	110	handle(HTML_Panel.Mouse_Click(elem, event))
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	111	override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	112	handle(HTML_Panel.Double_Click(elem, event))
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	113	override def onMouseOver(elem: HTMLElement, event: MouseEvent)
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	114	{ handle(HTML_Panel.Mouse_Over(elem, event)) }
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	115	override def onMouseOut(elem: HTMLElement, event: MouseEvent)
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	116	{ handle(HTML_Panel.Mouse_Out(elem, event)) }
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	117	}
49245d68f7e4 basic setup for HTML_Panel event handling; wenzelm parents: 34770 diff changeset	118
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	119	private val builder = new DocumentBuilderImpl(ucontext, rcontext)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	120
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	121	private case class Init(font_size: Int)
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	122	private case class Render(body: List[XML.Tree])
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	123
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	124	private val main_actor = actor {
34791 b97d5b38dea4 explicit object Session.Global_Settings; wenzelm parents: 34776 diff changeset	125	// crude double buffering
34823 2f3ea37c5958 renamed Proof_Document to Document; wenzelm parents: 34791 diff changeset	126	var doc1: org.w3c.dom.Document = null
2f3ea37c5958 renamed Proof_Document to Document; wenzelm parents: 34791 diff changeset	127	var doc2: org.w3c.dom.Document = null
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	128
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	129	var current_font_size = 16
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	130	var current_font_metrics: FontMetrics = null
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	131
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	132	def metric(s: String): Double =
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	133	if (current_font_metrics == null) s.length.toDouble
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	134	else current_font_metrics.stringWidth(s).toDouble / current_font_metrics.charWidth(Symbol.spc)
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	135
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	136	loop {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	137	react {
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	138	case Init(font_size) =>
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	139	current_font_size = font_size
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	140	current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	141
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	142	val src = template(font_size)
34766 4f9bcd4b5bd1 provide dummy URL; wenzelm parents: 34765 diff changeset	143	def parse() =
4f9bcd4b5bd1 provide dummy URL; wenzelm parents: 34765 diff changeset	144	builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	145	doc1 = parse()
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	146	doc2 = parse()
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	147	Swing_Thread.now { setDocument(doc1, rcontext) }
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	148
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	149	case Render(body) =>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	150	val doc = doc2
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	151	val html_body =
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	152	Pretty.formatted(body, panel_width(current_font_size), metric)
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	153	.map(t => XML.elem(HTML.PRE, HTML.spans(t)))
36735 42b7f881f5fc output symbolic pretty printing markup and format in the front end; wenzelm parents: 36015 diff changeset	154	val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	155	doc.removeChild(doc.getLastChild())
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	156	doc.appendChild(node)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	157	doc2 = doc1
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	158	doc1 = doc
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	159	Swing_Thread.now { setDocument(doc1, rcontext) }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	160
34769 826525fc5285 more precise messages; wenzelm parents: 34766 diff changeset	161	case bad => System.err.println("main_actor: ignoring bad message " + bad)
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	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	164	}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	165
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	166
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	167	/* main method wrappers */
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	168
ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	169	def init(font_size: Int) { main_actor ! Init(font_size) }
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	170	def render(body: List[XML.Tree]) { main_actor ! Render(body) }
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36790 diff changeset	171
36817 ed97e877ff2d more precise pretty printing based on actual font metrics; wenzelm parents: 36814 diff changeset	172	init(initial_font_size)
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: diff changeset	173	}

author	wenzelm
	Tue, 11 May 2010 23:36:06 +0200
changeset 36817	ed97e877ff2d
parent 36814	dc85664dbf6d
child 36819	fc8a6b5f9b0b
permissions	-rw-r--r--