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