src/Tools/jEdit/src/html_panel.scala
changeset 43282 5d294220ca43
parent 42976 9901f877eeb7
child 43442 e1fff67b23ac
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -0,0 +1,206 @@
     1.4 +/*  Title:      Tools/jEdit/src/html_panel.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +HTML panel based on Lobo/Cobra.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import java.io.StringReader
    1.16 +import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
    1.17 +import java.awt.event.MouseEvent
    1.18 +
    1.19 +import java.util.logging.{Logger, Level}
    1.20 +
    1.21 +import org.w3c.dom.html2.HTMLElement
    1.22 +
    1.23 +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
    1.24 +import org.lobobrowser.html.gui.HtmlPanel
    1.25 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
    1.26 +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
    1.27 +
    1.28 +import scala.actors.Actor._
    1.29 +
    1.30 +
    1.31 +object HTML_Panel
    1.32 +{
    1.33 +  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
    1.34 +  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
    1.35 +  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    1.36 +  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    1.37 +  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
    1.38 +  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
    1.39 +}
    1.40 +
    1.41 +
    1.42 +class HTML_Panel(
    1.43 +    system: Isabelle_System,
    1.44 +    initial_font_family: String,
    1.45 +    initial_font_size: Int)
    1.46 +  extends HtmlPanel
    1.47 +{
    1.48 +  /** Lobo setup **/
    1.49 +
    1.50 +  /* global logging */
    1.51 +
    1.52 +  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
    1.53 +
    1.54 +
    1.55 +  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
    1.56 +
    1.57 +  val screen_resolution =
    1.58 +    if (GraphicsEnvironment.isHeadless()) 72
    1.59 +    else Toolkit.getDefaultToolkit().getScreenResolution()
    1.60 +
    1.61 +  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
    1.62 +  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
    1.63 +
    1.64 +
    1.65 +  /* contexts and event handling */
    1.66 +
    1.67 +  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
    1.68 +
    1.69 +  private val ucontext = new SimpleUserAgentContext
    1.70 +  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    1.71 +  {
    1.72 +    private def handle(event: HTML_Panel.Event): Boolean =
    1.73 +      if (handler.isDefinedAt(event)) { handler(event); false }
    1.74 +      else true
    1.75 +
    1.76 +    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    1.77 +      handle(HTML_Panel.Context_Menu(elem, event))
    1.78 +    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    1.79 +      handle(HTML_Panel.Mouse_Click(elem, event))
    1.80 +    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
    1.81 +      handle(HTML_Panel.Double_Click(elem, event))
    1.82 +    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
    1.83 +      { handle(HTML_Panel.Mouse_Over(elem, event)) }
    1.84 +    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
    1.85 +      { handle(HTML_Panel.Mouse_Out(elem, event)) }
    1.86 +  }
    1.87 +
    1.88 +  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
    1.89 +
    1.90 +
    1.91 +  /* document template with style sheets */
    1.92 +
    1.93 +  private val template_head =
    1.94 +    """<?xml version="1.0" encoding="utf-8"?>
    1.95 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
    1.96 +  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
    1.97 +<html xmlns="http://www.w3.org/1999/xhtml">
    1.98 +<head>
    1.99 +<style media="all" type="text/css">
   1.100 +""" +
   1.101 +  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
   1.102 +
   1.103 +  private val template_tail =
   1.104 +"""
   1.105 +</style>
   1.106 +</head>
   1.107 +<body/>
   1.108 +</html>
   1.109 +"""
   1.110 +
   1.111 +  private def template(font_family: String, font_size: Int): String =
   1.112 +    template_head +
   1.113 +    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
   1.114 +    template_tail
   1.115 +
   1.116 +
   1.117 +  /** main actor **/
   1.118 +
   1.119 +  /* internal messages */
   1.120 +
   1.121 +  private case class Resize(font_family: String, font_size: Int)
   1.122 +  private case class Render_Document(text: String)
   1.123 +  private case class Render(body: XML.Body)
   1.124 +  private case class Render_Sync(body: XML.Body)
   1.125 +  private case object Refresh
   1.126 +
   1.127 +  private val main_actor = actor {
   1.128 +
   1.129 +    /* internal state */
   1.130 +
   1.131 +    var current_font_metrics: FontMetrics = null
   1.132 +    var current_font_family = ""
   1.133 +    var current_font_size: Int = 0
   1.134 +    var current_margin: Int = 0
   1.135 +    var current_body: XML.Body = Nil
   1.136 +
   1.137 +    def resize(font_family: String, font_size: Int)
   1.138 +    {
   1.139 +      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
   1.140 +      val (font_metrics, margin) =
   1.141 +        Swing_Thread.now {
   1.142 +          val metrics = getFontMetrics(font)
   1.143 +          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
   1.144 +        }
   1.145 +      if (current_font_metrics == null ||
   1.146 +          current_font_family != font_family ||
   1.147 +          current_font_size != font_size ||
   1.148 +          current_margin != margin)
   1.149 +      {
   1.150 +        current_font_metrics = font_metrics
   1.151 +        current_font_family = font_family
   1.152 +        current_font_size = font_size
   1.153 +        current_margin = margin
   1.154 +        refresh()
   1.155 +      }
   1.156 +    }
   1.157 +
   1.158 +    def refresh() { render(current_body) }
   1.159 +
   1.160 +    def render_document(text: String)
   1.161 +    {
   1.162 +      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
   1.163 +      Swing_Thread.later { setDocument(doc, rcontext) }
   1.164 +    }
   1.165 +
   1.166 +    def render(body: XML.Body)
   1.167 +    {
   1.168 +      current_body = body
   1.169 +      val html_body =
   1.170 +        current_body.flatMap(div =>
   1.171 +          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
   1.172 +            .map(t =>
   1.173 +              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
   1.174 +                HTML.spans(t, true))))
   1.175 +      val doc =
   1.176 +        builder.parse(
   1.177 +          new InputSourceImpl(
   1.178 +            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
   1.179 +      doc.removeChild(doc.getLastChild())
   1.180 +      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
   1.181 +      Swing_Thread.later { setDocument(doc, rcontext) }
   1.182 +    }
   1.183 +
   1.184 +
   1.185 +    /* main loop */
   1.186 +
   1.187 +    resize(initial_font_family, initial_font_size)
   1.188 +
   1.189 +    loop {
   1.190 +      react {
   1.191 +        case Resize(font_family, font_size) => resize(font_family, font_size)
   1.192 +        case Refresh => refresh()
   1.193 +        case Render_Document(text) => render_document(text)
   1.194 +        case Render(body) => render(body)
   1.195 +        case Render_Sync(body) => render(body); reply(())
   1.196 +        case bad => System.err.println("main_actor: ignoring bad message " + bad)
   1.197 +      }
   1.198 +    }
   1.199 +  }
   1.200 +
   1.201 +
   1.202 +  /* external methods */
   1.203 +
   1.204 +  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   1.205 +  def refresh() { main_actor ! Refresh }
   1.206 +  def render_document(text: String) { main_actor ! Render_Document(text) }
   1.207 +  def render(body: XML.Body) { main_actor ! Render(body) }
   1.208 +  def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
   1.209 +}