src/Tools/jEdit/src/jedit/html_panel.scala
author wenzelm
Tue May 11 23:36:06 2010 +0200 (2010-05-11)
changeset 36817 ed97e877ff2d
parent 36814 dc85664dbf6d
child 36819 fc8a6b5f9b0b
permissions -rw-r--r--
more precise pretty printing based on actual font metrics;
removed obsolete relative margin;
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.io.Source
wenzelm@34765
    27
import scala.actors.Actor._
wenzelm@34765
    28
wenzelm@34765
    29
wenzelm@34775
    30
object HTML_Panel
wenzelm@34775
    31
{
wenzelm@34775
    32
  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
wenzelm@34775
    33
  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    34
  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    35
  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    36
  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    37
  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
wenzelm@34775
    38
}
wenzelm@34775
    39
wenzelm@34775
    40
wenzelm@34775
    41
class HTML_Panel(
wenzelm@34775
    42
  sys: Isabelle_System,
wenzelm@36817
    43
  initial_font_size: Int,
wenzelm@34775
    44
  handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
wenzelm@34765
    45
{
wenzelm@34765
    46
  // global logging
wenzelm@34765
    47
  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
wenzelm@34765
    48
wenzelm@34765
    49
wenzelm@36817
    50
  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
wenzelm@36817
    51
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@34765
    60
  /* document template */
wenzelm@34765
    61
wenzelm@34765
    62
  private def try_file(name: String): String =
wenzelm@34765
    63
  {
wenzelm@34765
    64
    val file = sys.platform_file(name)
wenzelm@34776
    65
    if (file.isFile) Source.fromFile(file).mkString else ""
wenzelm@34765
    66
  }
wenzelm@34765
    67
wenzelm@34765
    68
  private def template(font_size: Int): String =
wenzelm@36790
    69
  {
wenzelm@34765
    70
    """<?xml version="1.0" encoding="utf-8"?>
wenzelm@34765
    71
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34765
    72
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34765
    73
<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34765
    74
<head>
wenzelm@34770
    75
<style media="all" type="text/css">
wenzelm@34770
    76
""" +
wenzelm@34765
    77
  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
wenzelm@34765
    78
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@36817
    79
  "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
wenzelm@34765
    80
"""
wenzelm@34765
    81
</style>
wenzelm@34765
    82
</head>
wenzelm@34765
    83
<body/>
wenzelm@34765
    84
</html>
wenzelm@34765
    85
"""
wenzelm@36790
    86
  }
wenzelm@34765
    87
wenzelm@36817
    88
  def font_metrics(font_size: Int): FontMetrics =
wenzelm@36817
    89
    Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
wenzelm@34765
    90
wenzelm@36817
    91
  def panel_width(font_size: Int): Int =
wenzelm@36814
    92
    Swing_Thread.now {
wenzelm@36817
    93
      (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
wenzelm@36814
    94
    }
wenzelm@36814
    95
wenzelm@36814
    96
wenzelm@34765
    97
  /* actor with local state */
wenzelm@34765
    98
wenzelm@34765
    99
  private val ucontext = new SimpleUserAgentContext
wenzelm@34775
   100
wenzelm@34765
   101
  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
wenzelm@34775
   102
  {
wenzelm@34775
   103
    private def handle(event: HTML_Panel.Event): Boolean =
wenzelm@34775
   104
      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
wenzelm@34775
   105
      else false
wenzelm@34775
   106
wenzelm@34775
   107
    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
   108
      handle(HTML_Panel.Context_Menu(elem, event))
wenzelm@34775
   109
    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
   110
      handle(HTML_Panel.Mouse_Click(elem, event))
wenzelm@34775
   111
    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
   112
      handle(HTML_Panel.Double_Click(elem, event))
wenzelm@34775
   113
    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
wenzelm@34775
   114
      { handle(HTML_Panel.Mouse_Over(elem, event)) }
wenzelm@34775
   115
    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
wenzelm@34775
   116
      { handle(HTML_Panel.Mouse_Out(elem, event)) }
wenzelm@34775
   117
  }
wenzelm@34775
   118
wenzelm@34765
   119
  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@34765
   120
wenzelm@36817
   121
  private case class Init(font_size: Int)
wenzelm@34765
   122
  private case class Render(body: List[XML.Tree])
wenzelm@34765
   123
wenzelm@34765
   124
  private val main_actor = actor {
wenzelm@34791
   125
    // crude double buffering
wenzelm@34823
   126
    var doc1: org.w3c.dom.Document = null
wenzelm@34823
   127
    var doc2: org.w3c.dom.Document = null
wenzelm@34765
   128
wenzelm@36814
   129
    var current_font_size = 16
wenzelm@36817
   130
    var current_font_metrics: FontMetrics = null
wenzelm@36817
   131
wenzelm@36817
   132
    def metric(s: String): Double =
wenzelm@36817
   133
      if (current_font_metrics == null) s.length.toDouble
wenzelm@36817
   134
      else current_font_metrics.stringWidth(s).toDouble / current_font_metrics.charWidth(Symbol.spc)
wenzelm@36814
   135
wenzelm@34765
   136
    loop {
wenzelm@34765
   137
      react {
wenzelm@36817
   138
        case Init(font_size) =>
wenzelm@36814
   139
          current_font_size = font_size
wenzelm@36817
   140
          current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
wenzelm@36814
   141
wenzelm@34765
   142
          val src = template(font_size)
wenzelm@34766
   143
          def parse() =
wenzelm@34766
   144
            builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
wenzelm@34765
   145
          doc1 = parse()
wenzelm@34765
   146
          doc2 = parse()
wenzelm@34765
   147
          Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@36817
   148
wenzelm@34765
   149
        case Render(body) =>
wenzelm@34765
   150
          val doc = doc2
wenzelm@36814
   151
          val html_body =
wenzelm@36817
   152
            Pretty.formatted(body, panel_width(current_font_size), metric)
wenzelm@36814
   153
              .map(t => XML.elem(HTML.PRE, HTML.spans(t)))
wenzelm@36735
   154
          val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
wenzelm@34765
   155
          doc.removeChild(doc.getLastChild())
wenzelm@34765
   156
          doc.appendChild(node)
wenzelm@34765
   157
          doc2 = doc1
wenzelm@34765
   158
          doc1 = doc
wenzelm@34765
   159
          Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@34765
   160
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@34765
   166
wenzelm@34765
   167
  /* main method wrappers */
wenzelm@36817
   168
wenzelm@36817
   169
  def init(font_size: Int) { main_actor ! Init(font_size) }
wenzelm@34765
   170
  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
wenzelm@36814
   171
wenzelm@36817
   172
  init(initial_font_size)
wenzelm@34765
   173
}