isabelle: src/Tools/jEdit/src/jedit/html_panel.scala@8b4617ad1593 (annotated)

wenzelm@36760	1	/* Title: Tools/jEdit/src/jedit/html_panel.scala
wenzelm@36760	2	Author: Makarius
wenzelm@36760	3
wenzelm@36760	4	HTML panel based on Lobo/Cobra.
wenzelm@36760	5	*/
wenzelm@34765	6
wenzelm@34871	7	package isabelle.jedit
wenzelm@34765	8
wenzelm@34765	9
wenzelm@36015	10	import isabelle._
wenzelm@36015	11
wenzelm@34765	12	import java.io.StringReader
wenzelm@37164	13	import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
wenzelm@34775	14	import java.awt.event.MouseEvent
wenzelm@34775	15
wenzelm@34765	16	import java.util.logging.{Logger, Level}
wenzelm@34765	17
wenzelm@34775	18	import org.w3c.dom.html2.HTMLElement
wenzelm@34765	19
wenzelm@34765	20	import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
wenzelm@34765	21	import org.lobobrowser.html.gui.HtmlPanel
wenzelm@34765	22	import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
wenzelm@34765	23	import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
wenzelm@34765	24
wenzelm@34765	25	import scala.actors.Actor._
wenzelm@34765	26
wenzelm@34765	27
wenzelm@34775	28	object HTML_Panel
wenzelm@34775	29	{
wenzelm@34775	30	sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
wenzelm@34775	31	case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775	32	case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775	33	case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775	34	case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775	35	case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775	36	}
wenzelm@34775	37
wenzelm@34775	38
wenzelm@37164	39	class HTML_Panel(
wenzelm@37164	40	system: Isabelle_System,
wenzelm@37164	41	initial_font_family: String,
wenzelm@37164	42	initial_font_size: Int)
wenzelm@37164	43	extends HtmlPanel
wenzelm@34765	44	{
wenzelm@37034	45	/ Lobo setup /
wenzelm@37034	46
wenzelm@37034	47	/* global logging */
wenzelm@37034	48
wenzelm@34765	49	Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
wenzelm@34765	50
wenzelm@34765	51
wenzelm@37034	52	/* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
wenzelm@36817	53
wenzelm@36817	54	val screen_resolution =
wenzelm@36817	55	if (GraphicsEnvironment.isHeadless()) 72
wenzelm@36817	56	else Toolkit.getDefaultToolkit().getScreenResolution()
wenzelm@36817	57
wenzelm@36817	58	def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
wenzelm@36817	59	def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
wenzelm@36817	60
wenzelm@36817	61
wenzelm@37036	62	/* contexts and event handling */
wenzelm@37036	63
wenzelm@37036	64	protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
wenzelm@37036	65
wenzelm@36993	66	private val ucontext = new SimpleUserAgentContext
wenzelm@36993	67	private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
wenzelm@36993	68	{
wenzelm@36993	69	private def handle(event: HTML_Panel.Event): Boolean =
wenzelm@37036	70	if (handler.isDefinedAt(event)) { handler(event); true }
wenzelm@36993	71	else false
wenzelm@36993	72
wenzelm@36993	73	override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993	74	handle(HTML_Panel.Context_Menu(elem, event))
wenzelm@36993	75	override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993	76	handle(HTML_Panel.Mouse_Click(elem, event))
wenzelm@36993	77	override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993	78	handle(HTML_Panel.Double_Click(elem, event))
wenzelm@36993	79	override def onMouseOver(elem: HTMLElement, event: MouseEvent)
wenzelm@36993	80	{ handle(HTML_Panel.Mouse_Over(elem, event)) }
wenzelm@36993	81	override def onMouseOut(elem: HTMLElement, event: MouseEvent)
wenzelm@36993	82	{ handle(HTML_Panel.Mouse_Out(elem, event)) }
wenzelm@36993	83	}
wenzelm@36993	84
wenzelm@36993	85	private val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@36993	86
wenzelm@36993	87
wenzelm@37015	88	/* document template with style sheets */
wenzelm@34765	89
wenzelm@37015	90	private val template_head =
wenzelm@34765	91	"""<?xml version="1.0" encoding="utf-8"?>
wenzelm@34765	92	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34765	93	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34765	94	<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34765	95	<head>
wenzelm@34770	96	<style media="all" type="text/css">
wenzelm@34770	97	""" +
wenzelm@37058	98	system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
wenzelm@37015	99
wenzelm@37015	100	private val template_tail =
wenzelm@34765	101	"""
wenzelm@34765	102	</style>
wenzelm@34765	103	</head>
wenzelm@34765	104	<body/>
wenzelm@34765	105	</html>
wenzelm@34765	106	"""
wenzelm@37015	107
wenzelm@37164	108	private def template(font_family: String, font_size: Int): String =
wenzelm@37015	109	template_head +
wenzelm@37164	110	"body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px }" +
wenzelm@37015	111	template_tail
wenzelm@37015	112
wenzelm@37015	113
wenzelm@37034	114	/ main actor /
wenzelm@37034	115
wenzelm@37034	116	/* internal messages */
wenzelm@37034	117
wenzelm@37164	118	private case class Resize(font_family: String, font_size: Int)
wenzelm@37034	119	private case class Render(body: List[XML.Tree])
wenzelm@37034	120	private case object Refresh
wenzelm@34765	121
wenzelm@37034	122	private val main_actor = actor {
wenzelm@37034	123
wenzelm@37034	124	/* internal state */
wenzelm@37034	125
wenzelm@37034	126	var current_font_metrics: FontMetrics = null
wenzelm@37164	127	var current_font_family = ""
wenzelm@37034	128	var current_font_size: Int = 0
wenzelm@37034	129	var current_margin: Int = 0
wenzelm@37034	130	var current_body: List[XML.Tree] = Nil
wenzelm@34765	131
wenzelm@37164	132	def resize(font_family: String, font_size: Int)
wenzelm@36993	133	{
wenzelm@37164	134	val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
wenzelm@37034	135	val (font_metrics, margin) =
wenzelm@36993	136	Swing_Thread.now {
wenzelm@37164	137	val metrics = getFontMetrics(font)
wenzelm@37034	138	(metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
wenzelm@36993	139	}
wenzelm@37034	140	if (current_font_metrics == null \|\|
wenzelm@37164	141	current_font_family != font_family \|\|
wenzelm@37034	142	current_font_size != font_size \|\|
wenzelm@37034	143	current_margin != margin)
wenzelm@37034	144	{
wenzelm@37034	145	current_font_metrics = font_metrics
wenzelm@37164	146	current_font_family = font_family
wenzelm@37034	147	current_font_size = font_size
wenzelm@37034	148	current_margin = margin
wenzelm@37014	149	refresh()
wenzelm@36993	150	}
wenzelm@36814	151	}
wenzelm@36814	152
wenzelm@37014	153	def refresh() { render(current_body) }
wenzelm@37014	154
wenzelm@36993	155	def render(body: List[XML.Tree])
wenzelm@36993	156	{
wenzelm@36993	157	current_body = body
wenzelm@36993	158	val html_body =
wenzelm@36993	159	current_body.flatMap(div =>
wenzelm@37034	160	Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
wenzelm@37040	161	.map(t => XML.Elem(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE)), HTML.spans(t))))
wenzelm@37034	162	val doc =
wenzelm@37034	163	builder.parse(
wenzelm@37164	164	new InputSourceImpl(
wenzelm@37164	165	new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
wenzelm@37034	166	doc.removeChild(doc.getLastChild())
wenzelm@37034	167	doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
wenzelm@37034	168	Swing_Thread.later { setDocument(doc, rcontext) }
wenzelm@37034	169	}
wenzelm@34775	170
wenzelm@37034	171
wenzelm@37034	172	/* main loop */
wenzelm@36993	173
wenzelm@37164	174	resize(initial_font_family, initial_font_size)
wenzelm@34775	175
wenzelm@34765	176	loop {
wenzelm@34765	177	react {
wenzelm@37164	178	case Resize(font_family, font_size) => resize(font_family, font_size)
wenzelm@37034	179	case Refresh => refresh()
wenzelm@37034	180	case Render(body) => render(body)
wenzelm@34769	181	case bad => System.err.println("main_actor: ignoring bad message " + bad)
wenzelm@34765	182	}
wenzelm@34765	183	}
wenzelm@34765	184	}
wenzelm@34765	185
wenzelm@37034	186
wenzelm@37034	187	/* external methods */
wenzelm@37034	188
wenzelm@37164	189	def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
wenzelm@37014	190	def refresh() { main_actor ! Refresh }
wenzelm@36993	191	def render(body: List[XML.Tree]) { main_actor ! Render(body) }
wenzelm@34765	192	}

author	wenzelm
	Fri May 28 17:48:18 2010 +0200 (2010-05-28)
changeset 37164	8b4617ad1593
parent 37069	7d796b72099f
child 37202	382a56c9f295
permissions	-rw-r--r--