wenzelm@36760: /* Title: Tools/jEdit/src/jedit/html_panel.scala wenzelm@36760: Author: Makarius wenzelm@36760: wenzelm@36760: HTML panel based on Lobo/Cobra. wenzelm@36760: */ wenzelm@34765: wenzelm@34871: package isabelle.jedit wenzelm@34765: wenzelm@34765: wenzelm@36015: import isabelle._ wenzelm@36015: wenzelm@34765: import java.io.StringReader wenzelm@36817: import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics} wenzelm@34775: import java.awt.event.MouseEvent wenzelm@34775: wenzelm@34765: import javax.swing.{JButton, JPanel, JScrollPane} wenzelm@34765: import java.util.logging.{Logger, Level} wenzelm@34765: wenzelm@34775: import org.w3c.dom.html2.HTMLElement wenzelm@34765: wenzelm@34765: import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl} wenzelm@34765: import org.lobobrowser.html.gui.HtmlPanel wenzelm@34765: import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl} wenzelm@34765: import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext} wenzelm@34765: wenzelm@34765: import scala.actors.Actor._ wenzelm@34765: wenzelm@34765: wenzelm@34775: object HTML_Panel wenzelm@34775: { wenzelm@34775: sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent } wenzelm@34775: case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event wenzelm@34775: case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event wenzelm@34775: case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event wenzelm@34775: case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event wenzelm@34775: case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event wenzelm@34775: } wenzelm@34775: wenzelm@34775: wenzelm@34775: class HTML_Panel( wenzelm@36992: system: Isabelle_System, wenzelm@36817: initial_font_size: Int, wenzelm@34775: handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel wenzelm@34765: { wenzelm@37034: /** Lobo setup **/ wenzelm@37034: wenzelm@37034: /* global logging */ wenzelm@37034: wenzelm@34765: Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) wenzelm@34765: wenzelm@34765: wenzelm@37034: /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */ wenzelm@36817: wenzelm@36817: val screen_resolution = wenzelm@36817: if (GraphicsEnvironment.isHeadless()) 72 wenzelm@36817: else Toolkit.getDefaultToolkit().getScreenResolution() wenzelm@36817: wenzelm@36817: def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution wenzelm@36817: def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96 wenzelm@36817: wenzelm@36817: wenzelm@36993: private val ucontext = new SimpleUserAgentContext wenzelm@36993: private val rcontext = new SimpleHtmlRendererContext(this, ucontext) wenzelm@36993: { wenzelm@36993: private def handle(event: HTML_Panel.Event): Boolean = wenzelm@36993: if (handler != null && handler.isDefinedAt(event)) { handler(event); true } wenzelm@36993: else false wenzelm@36993: wenzelm@36993: override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = wenzelm@36993: handle(HTML_Panel.Context_Menu(elem, event)) wenzelm@36993: override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean = wenzelm@36993: handle(HTML_Panel.Mouse_Click(elem, event)) wenzelm@36993: override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean = wenzelm@36993: handle(HTML_Panel.Double_Click(elem, event)) wenzelm@36993: override def onMouseOver(elem: HTMLElement, event: MouseEvent) wenzelm@36993: { handle(HTML_Panel.Mouse_Over(elem, event)) } wenzelm@36993: override def onMouseOut(elem: HTMLElement, event: MouseEvent) wenzelm@36993: { handle(HTML_Panel.Mouse_Out(elem, event)) } wenzelm@36993: } wenzelm@36993: wenzelm@36993: private val builder = new DocumentBuilderImpl(ucontext, rcontext) wenzelm@36993: wenzelm@36993: wenzelm@37015: /* document template with style sheets */ wenzelm@34765: wenzelm@37015: private val template_head = wenzelm@34765: """ wenzelm@34765: wenzelm@34765: wenzelm@34765:
wenzelm@34770: wenzelm@34765: wenzelm@34765: