src/Tools/jEdit/src/jedit/html_panel.scala
author wenzelm
Thu May 20 20:56:26 2010 +0200 (2010-05-20)
changeset 37014 1af0f718ffdc
parent 36995 9421452afc29
child 37015 39207774a9b7
permissions -rw-r--r--
handle component resize for output / HTML panel;
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/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@36817
    13
import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
wenzelm@34775
    14
import java.awt.event.MouseEvent
wenzelm@34775
    15
wenzelm@34765
    16
import javax.swing.{JButton, JPanel, JScrollPane}
wenzelm@34765
    17
import java.util.logging.{Logger, Level}
wenzelm@34765
    18
wenzelm@34775
    19
import org.w3c.dom.html2.HTMLElement
wenzelm@34765
    20
wenzelm@34765
    21
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
wenzelm@34765
    22
import org.lobobrowser.html.gui.HtmlPanel
wenzelm@34765
    23
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
wenzelm@34765
    24
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
wenzelm@34765
    25
wenzelm@34765
    26
import scala.actors.Actor._
wenzelm@34765
    27
wenzelm@34765
    28
wenzelm@34775
    29
object HTML_Panel
wenzelm@34775
    30
{
wenzelm@34775
    31
  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
wenzelm@34775
    32
  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    33
  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    34
  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    35
  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    36
  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    37
}
wenzelm@34775
    38
wenzelm@34775
    39
wenzelm@34775
    40
class HTML_Panel(
wenzelm@36992
    41
  system: Isabelle_System,
wenzelm@36817
    42
  initial_font_size: Int,
wenzelm@34775
    43
  handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
wenzelm@34765
    44
{
wenzelm@34765
    45
  // global logging
wenzelm@34765
    46
  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
wenzelm@34765
    47
wenzelm@34765
    48
wenzelm@36993
    49
  /* Lobo setup */
wenzelm@36817
    50
wenzelm@36993
    51
  // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
wenzelm@36817
    52
  val screen_resolution =
wenzelm@36817
    53
    if (GraphicsEnvironment.isHeadless()) 72
wenzelm@36817
    54
    else Toolkit.getDefaultToolkit().getScreenResolution()
wenzelm@36817
    55
wenzelm@36817
    56
  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
wenzelm@36817
    57
  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
wenzelm@36817
    58
wenzelm@36817
    59
wenzelm@36993
    60
  private val ucontext = new SimpleUserAgentContext
wenzelm@36993
    61
  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
wenzelm@36993
    62
  {
wenzelm@36993
    63
    private def handle(event: HTML_Panel.Event): Boolean =
wenzelm@36993
    64
      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
wenzelm@36993
    65
      else false
wenzelm@36993
    66
wenzelm@36993
    67
    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993
    68
      handle(HTML_Panel.Context_Menu(elem, event))
wenzelm@36993
    69
    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993
    70
      handle(HTML_Panel.Mouse_Click(elem, event))
wenzelm@36993
    71
    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@36993
    72
      handle(HTML_Panel.Double_Click(elem, event))
wenzelm@36993
    73
    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
wenzelm@36993
    74
      { handle(HTML_Panel.Mouse_Over(elem, event)) }
wenzelm@36993
    75
    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
wenzelm@36993
    76
      { handle(HTML_Panel.Mouse_Out(elem, event)) }
wenzelm@36993
    77
  }
wenzelm@36993
    78
wenzelm@36993
    79
  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@36993
    80
wenzelm@36993
    81
wenzelm@36993
    82
  /* physical document */
wenzelm@34765
    83
wenzelm@34765
    84
  private def template(font_size: Int): String =
wenzelm@36790
    85
  {
wenzelm@34765
    86
    """<?xml version="1.0" encoding="utf-8"?>
wenzelm@34765
    87
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34765
    88
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34765
    89
<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34765
    90
<head>
wenzelm@34770
    91
<style media="all" type="text/css">
wenzelm@34770
    92
""" +
wenzelm@36992
    93
  system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
wenzelm@36992
    94
  system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@36992
    95
  "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
wenzelm@34765
    96
"""
wenzelm@34765
    97
</style>
wenzelm@34765
    98
</head>
wenzelm@34765
    99
<body/>
wenzelm@34765
   100
</html>
wenzelm@34765
   101
"""
wenzelm@36790
   102
  }
wenzelm@34765
   103
wenzelm@36993
   104
  private class Doc
wenzelm@36993
   105
  {
wenzelm@37014
   106
    private var current_font_size: Int = 0
wenzelm@37014
   107
    private var current_font_metrics: FontMetrics = null
wenzelm@37014
   108
    private var current_body: List[XML.Tree] = Nil
wenzelm@37014
   109
    private var current_DOM: org.w3c.dom.Document = null
wenzelm@34765
   110
wenzelm@36993
   111
    def resize(font_size: Int)
wenzelm@36993
   112
    {
wenzelm@36993
   113
      if (font_size != current_font_size || current_font_metrics == null) {
wenzelm@36993
   114
        Swing_Thread.now {
wenzelm@36993
   115
          current_font_size = font_size
wenzelm@36993
   116
          current_font_metrics =
wenzelm@36993
   117
            getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
wenzelm@36993
   118
        }
wenzelm@36993
   119
        current_DOM =
wenzelm@36993
   120
          builder.parse(
wenzelm@36993
   121
            new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
wenzelm@37014
   122
        refresh()
wenzelm@36993
   123
      }
wenzelm@36814
   124
    }
wenzelm@36814
   125
wenzelm@37014
   126
    def refresh() { render(current_body) }
wenzelm@37014
   127
wenzelm@36993
   128
    def render(body: List[XML.Tree])
wenzelm@36993
   129
    {
wenzelm@36993
   130
      current_body = body
wenzelm@36995
   131
      val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
wenzelm@36993
   132
      val html_body =
wenzelm@36993
   133
        current_body.flatMap(div =>
wenzelm@36995
   134
          Pretty.formatted(List(div), margin,
wenzelm@36993
   135
              Pretty.font_metric(current_font_metrics))
wenzelm@36993
   136
            .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
wenzelm@34775
   137
wenzelm@36993
   138
      val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
wenzelm@36993
   139
      current_DOM.removeChild(current_DOM.getLastChild())
wenzelm@36993
   140
      current_DOM.appendChild(node)
wenzelm@36993
   141
      Swing_Thread.now { setDocument(current_DOM, rcontext) }
wenzelm@36993
   142
    }
wenzelm@36993
   143
wenzelm@36993
   144
    resize(initial_font_size)
wenzelm@34775
   145
  }
wenzelm@34775
   146
wenzelm@36993
   147
wenzelm@36993
   148
  /* main actor and method wrappers */
wenzelm@34765
   149
wenzelm@36993
   150
  private case class Resize(font_size: Int)
wenzelm@36993
   151
  private case class Render(body: List[XML.Tree])
wenzelm@37014
   152
  private case object Refresh
wenzelm@34765
   153
wenzelm@34765
   154
  private val main_actor = actor {
wenzelm@36993
   155
    var doc = new Doc
wenzelm@34765
   156
    loop {
wenzelm@34765
   157
      react {
wenzelm@36993
   158
        case Resize(font_size) => doc.resize(font_size)
wenzelm@37014
   159
        case Refresh => doc.refresh()
wenzelm@36993
   160
        case Render(body) => doc.render(body)
wenzelm@34769
   161
        case bad => System.err.println("main_actor: ignoring bad message " + bad)
wenzelm@34765
   162
      }
wenzelm@34765
   163
    }
wenzelm@34765
   164
  }
wenzelm@34765
   165
wenzelm@36993
   166
  def resize(font_size: Int) { main_actor ! Resize(font_size) }
wenzelm@37014
   167
  def refresh() { main_actor ! Refresh }
wenzelm@36993
   168
  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
wenzelm@34765
   169
}