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