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