--- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed Jun 08 17:01:07 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-/* Title: Tools/jEdit/src/jedit/html_panel.scala
- Author: Makarius
-
-HTML panel based on Lobo/Cobra.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.io.StringReader
-import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
-import java.awt.event.MouseEvent
-
-import java.util.logging.{Logger, Level}
-
-import org.w3c.dom.html2.HTMLElement
-
-import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
-import org.lobobrowser.html.gui.HtmlPanel
-import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
-import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
-
-import scala.actors.Actor._
-
-
-object HTML_Panel
-{
- sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
- case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
-}
-
-
-class HTML_Panel(
- system: Isabelle_System,
- initial_font_family: String,
- initial_font_size: Int)
- extends HtmlPanel
-{
- /** Lobo setup **/
-
- /* global logging */
-
- Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
-
- /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
-
- val screen_resolution =
- if (GraphicsEnvironment.isHeadless()) 72
- else Toolkit.getDefaultToolkit().getScreenResolution()
-
- def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
- def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
-
-
- /* contexts and event handling */
-
- protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
-
- private val ucontext = new SimpleUserAgentContext
- private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
- {
- private def handle(event: HTML_Panel.Event): Boolean =
- if (handler.isDefinedAt(event)) { handler(event); false }
- else true
-
- override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Context_Menu(elem, event))
- override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Mouse_Click(elem, event))
- override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Double_Click(elem, event))
- override def onMouseOver(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Over(elem, event)) }
- override def onMouseOut(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Out(elem, event)) }
- }
-
- private val builder = new DocumentBuilderImpl(ucontext, rcontext)
-
-
- /* document template with style sheets */
-
- private val template_head =
- """<?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
- "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
-<style media="all" type="text/css">
-""" +
- system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
-
- private val template_tail =
-"""
-</style>
-</head>
-<body/>
-</html>
-"""
-
- private def template(font_family: String, font_size: Int): String =
- template_head +
- "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
- template_tail
-
-
- /** main actor **/
-
- /* internal messages */
-
- private case class Resize(font_family: String, font_size: Int)
- private case class Render_Document(text: String)
- private case class Render(body: XML.Body)
- private case class Render_Sync(body: XML.Body)
- private case object Refresh
-
- private val main_actor = actor {
-
- /* internal state */
-
- var current_font_metrics: FontMetrics = null
- var current_font_family = ""
- var current_font_size: Int = 0
- var current_margin: Int = 0
- var current_body: XML.Body = Nil
-
- def resize(font_family: String, font_size: Int)
- {
- val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
- val (font_metrics, margin) =
- Swing_Thread.now {
- val metrics = getFontMetrics(font)
- (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
- }
- if (current_font_metrics == null ||
- current_font_family != font_family ||
- current_font_size != font_size ||
- current_margin != margin)
- {
- current_font_metrics = font_metrics
- current_font_family = font_family
- current_font_size = font_size
- current_margin = margin
- refresh()
- }
- }
-
- def refresh() { render(current_body) }
-
- def render_document(text: String)
- {
- val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
- Swing_Thread.later { setDocument(doc, rcontext) }
- }
-
- def render(body: XML.Body)
- {
- current_body = body
- val html_body =
- current_body.flatMap(div =>
- Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
- .map(t =>
- XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
- HTML.spans(t, true))))
- val doc =
- builder.parse(
- new InputSourceImpl(
- new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
- doc.removeChild(doc.getLastChild())
- doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
- Swing_Thread.later { setDocument(doc, rcontext) }
- }
-
-
- /* main loop */
-
- resize(initial_font_family, initial_font_size)
-
- loop {
- react {
- case Resize(font_family, font_size) => resize(font_family, font_size)
- case Refresh => refresh()
- case Render_Document(text) => render_document(text)
- case Render(body) => render(body)
- case Render_Sync(body) => render(body); reply(())
- case bad => System.err.println("main_actor: ignoring bad message " + bad)
- }
- }
- }
-
-
- /* external methods */
-
- def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
- def refresh() { main_actor ! Refresh }
- def render_document(text: String) { main_actor ! Render_Document(text) }
- def render(body: XML.Body) { main_actor ! Render(body) }
- def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
-}