src/Tools/jEdit/src/proofdocument/html_panel.scala
author wenzelm
Thu Dec 10 14:14:49 2009 +0100 (2009-12-10)
changeset 34775 49245d68f7e4
parent 34770 0c630c52fc74
child 34776 01a9bfd64b87
permissions -rw-r--r--
basic setup for HTML_Panel event handling;
wenzelm@34765
     1
/*
wenzelm@34765
     2
 * HTML panel based on Lobo/Cobra
wenzelm@34765
     3
 *
wenzelm@34765
     4
 * @author Makarius
wenzelm@34765
     5
 */
wenzelm@34765
     6
wenzelm@34765
     7
package isabelle.proofdocument
wenzelm@34765
     8
wenzelm@34765
     9
wenzelm@34765
    10
import java.io.StringReader
wenzelm@34765
    11
import java.awt.{BorderLayout, Dimension}
wenzelm@34775
    12
import java.awt.event.MouseEvent
wenzelm@34775
    13
wenzelm@34765
    14
import javax.swing.{JButton, JPanel, JScrollPane}
wenzelm@34765
    15
import java.util.logging.{Logger, Level}
wenzelm@34765
    16
wenzelm@34765
    17
import org.w3c.dom.Document
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.io.Source
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@34775
    41
  sys: Isabelle_System,
wenzelm@34775
    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@34765
    49
  /* document template */
wenzelm@34765
    50
wenzelm@34765
    51
  private def try_file(name: String): String =
wenzelm@34765
    52
  {
wenzelm@34765
    53
    val file = sys.platform_file(name)
wenzelm@34765
    54
    if (file.exists) Source.fromFile(file).mkString else ""
wenzelm@34765
    55
  }
wenzelm@34765
    56
wenzelm@34765
    57
  private def template(font_size: Int): String =
wenzelm@34765
    58
    """<?xml version="1.0" encoding="utf-8"?>
wenzelm@34765
    59
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34765
    60
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34765
    61
<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34765
    62
<head>
wenzelm@34770
    63
<style media="all" type="text/css">
wenzelm@34770
    64
""" +
wenzelm@34765
    65
  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
wenzelm@34765
    66
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@34770
    67
  "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
wenzelm@34765
    68
"""
wenzelm@34765
    69
</style>
wenzelm@34765
    70
</head>
wenzelm@34765
    71
<body/>
wenzelm@34765
    72
</html>
wenzelm@34765
    73
"""
wenzelm@34765
    74
wenzelm@34765
    75
wenzelm@34765
    76
  /* actor with local state */
wenzelm@34765
    77
wenzelm@34765
    78
  private val ucontext = new SimpleUserAgentContext
wenzelm@34775
    79
wenzelm@34765
    80
  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
wenzelm@34775
    81
  {
wenzelm@34775
    82
    private def handle(event: HTML_Panel.Event): Boolean =
wenzelm@34775
    83
      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
wenzelm@34775
    84
      else false
wenzelm@34775
    85
wenzelm@34775
    86
    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
    87
      handle(HTML_Panel.Context_Menu(elem, event))
wenzelm@34775
    88
    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
    89
      handle(HTML_Panel.Mouse_Click(elem, event))
wenzelm@34775
    90
    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
wenzelm@34775
    91
      handle(HTML_Panel.Double_Click(elem, event))
wenzelm@34775
    92
    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
wenzelm@34775
    93
      { handle(HTML_Panel.Mouse_Over(elem, event)) }
wenzelm@34775
    94
    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
wenzelm@34775
    95
      { handle(HTML_Panel.Mouse_Out(elem, event)) }
wenzelm@34775
    96
  }
wenzelm@34775
    97
wenzelm@34765
    98
  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@34765
    99
wenzelm@34765
   100
  private case class Init(font_size: Int)
wenzelm@34765
   101
  private case class Render(body: List[XML.Tree])
wenzelm@34765
   102
wenzelm@34765
   103
  private val main_actor = actor {
wenzelm@34765
   104
    // double buffering
wenzelm@34765
   105
    var doc1: Document = null
wenzelm@34765
   106
    var doc2: Document = null
wenzelm@34765
   107
wenzelm@34765
   108
    loop {
wenzelm@34765
   109
      react {
wenzelm@34765
   110
        case Init(font_size) =>
wenzelm@34765
   111
          val src = template(font_size)
wenzelm@34766
   112
          def parse() =
wenzelm@34766
   113
            builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
wenzelm@34765
   114
          doc1 = parse()
wenzelm@34765
   115
          doc2 = parse()
wenzelm@34765
   116
          Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@34765
   117
          
wenzelm@34765
   118
        case Render(body) =>
wenzelm@34765
   119
          val doc = doc2
wenzelm@34765
   120
          val node =
wenzelm@34765
   121
            XML.document_node(doc,
wenzelm@34765
   122
              XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
wenzelm@34765
   123
          doc.removeChild(doc.getLastChild())
wenzelm@34765
   124
          doc.appendChild(node)
wenzelm@34765
   125
          doc2 = doc1
wenzelm@34765
   126
          doc1 = doc
wenzelm@34765
   127
          Swing_Thread.now { setDocument(doc1, rcontext) }
wenzelm@34765
   128
wenzelm@34769
   129
        case bad => System.err.println("main_actor: ignoring bad message " + bad)
wenzelm@34765
   130
      }
wenzelm@34765
   131
    }
wenzelm@34765
   132
  }
wenzelm@34765
   133
wenzelm@34765
   134
  main_actor ! Init(initial_font_size)
wenzelm@34765
   135
  
wenzelm@34765
   136
wenzelm@34765
   137
  /* main method wrappers */
wenzelm@34765
   138
  
wenzelm@34765
   139
  def init(font_size: Int) { main_actor ! Init(font_size) }
wenzelm@34765
   140
  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
wenzelm@34765
   141
}