wenzelm@34765: /*
wenzelm@34765: * HTML panel based on Lobo/Cobra
wenzelm@34765: *
wenzelm@34765: * @author Makarius
wenzelm@34765: */
wenzelm@34765:
wenzelm@34765: package isabelle.proofdocument
wenzelm@34765:
wenzelm@34765:
wenzelm@34765: import java.io.StringReader
wenzelm@34765: import java.awt.{BorderLayout, Dimension}
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@34765: import org.w3c.dom.Document
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.io.Source
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@34775: sys: Isabelle_System,
wenzelm@34775: initial_font_size: Int,
wenzelm@34775: handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
wenzelm@34765: {
wenzelm@34765: // global logging
wenzelm@34765: Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
wenzelm@34765:
wenzelm@34765:
wenzelm@34765: /* document template */
wenzelm@34765:
wenzelm@34765: private def try_file(name: String): String =
wenzelm@34765: {
wenzelm@34765: val file = sys.platform_file(name)
wenzelm@34765: if (file.exists) Source.fromFile(file).mkString else ""
wenzelm@34765: }
wenzelm@34765:
wenzelm@34765: private def template(font_size: Int): String =
wenzelm@34765: """
wenzelm@34765:
wenzelm@34765:
wenzelm@34765:
wenzelm@34770:
wenzelm@34765:
wenzelm@34765:
wenzelm@34765:
wenzelm@34765: """
wenzelm@34765:
wenzelm@34765:
wenzelm@34765: /* actor with local state */
wenzelm@34765:
wenzelm@34765: private val ucontext = new SimpleUserAgentContext
wenzelm@34775:
wenzelm@34765: private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
wenzelm@34775: {
wenzelm@34775: private def handle(event: HTML_Panel.Event): Boolean =
wenzelm@34775: if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
wenzelm@34775: else false
wenzelm@34775:
wenzelm@34775: override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775: handle(HTML_Panel.Context_Menu(elem, event))
wenzelm@34775: override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775: handle(HTML_Panel.Mouse_Click(elem, event))
wenzelm@34775: override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775: handle(HTML_Panel.Double_Click(elem, event))
wenzelm@34775: override def onMouseOver(elem: HTMLElement, event: MouseEvent)
wenzelm@34775: { handle(HTML_Panel.Mouse_Over(elem, event)) }
wenzelm@34775: override def onMouseOut(elem: HTMLElement, event: MouseEvent)
wenzelm@34775: { handle(HTML_Panel.Mouse_Out(elem, event)) }
wenzelm@34775: }
wenzelm@34775:
wenzelm@34765: private val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@34765:
wenzelm@34765: private case class Init(font_size: Int)
wenzelm@34765: private case class Render(body: List[XML.Tree])
wenzelm@34765:
wenzelm@34765: private val main_actor = actor {
wenzelm@34765: // double buffering
wenzelm@34765: var doc1: Document = null
wenzelm@34765: var doc2: Document = null
wenzelm@34765:
wenzelm@34765: loop {
wenzelm@34765: react {
wenzelm@34765: case Init(font_size) =>
wenzelm@34765: val src = template(font_size)
wenzelm@34766: def parse() =
wenzelm@34766: builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
wenzelm@34765: doc1 = parse()
wenzelm@34765: doc2 = parse()
wenzelm@34765: Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@34765:
wenzelm@34765: case Render(body) =>
wenzelm@34765: val doc = doc2
wenzelm@34765: val node =
wenzelm@34765: XML.document_node(doc,
wenzelm@34765: XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
wenzelm@34765: doc.removeChild(doc.getLastChild())
wenzelm@34765: doc.appendChild(node)
wenzelm@34765: doc2 = doc1
wenzelm@34765: doc1 = doc
wenzelm@34765: Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@34765:
wenzelm@34769: case bad => System.err.println("main_actor: ignoring bad message " + bad)
wenzelm@34765: }
wenzelm@34765: }
wenzelm@34765: }
wenzelm@34765:
wenzelm@34765: main_actor ! Init(initial_font_size)
wenzelm@34765:
wenzelm@34765:
wenzelm@34765: /* main method wrappers */
wenzelm@34765:
wenzelm@34765: def init(font_size: Int) { main_actor ! Init(font_size) }
wenzelm@34765: def render(body: List[XML.Tree]) { main_actor ! Render(body) }
wenzelm@34765: }