src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Mon Dec 07 00:05:21 2009 +0100 (2009-12-07)
changeset 34749 e377d3d6910a
parent 34748 a2ed621f5f52
child 34754 e8bb3052f3cb
permissions -rw-r--r--
use IsabelleText font;
explicit <pre> element;
relayout in swing thread -- paranoia mode;
wenzelm@34408
     1
/*
wenzelm@34408
     2
 * Dockable window with rendered state output
wenzelm@34408
     3
 *
wenzelm@34408
     4
 * @author Fabian Immler, TU Munich
wenzelm@34408
     5
 * @author Johannes Hölzl, TU Munich
wenzelm@34408
     6
 */
wenzelm@34408
     7
wenzelm@34318
     8
package isabelle.jedit
wenzelm@34318
     9
wenzelm@34745
    10
import isabelle.renderer.UserAgent
wenzelm@34745
    11
import isabelle.XML
wenzelm@34318
    12
wenzelm@34745
    13
import java.io.StringReader
wenzelm@34424
    14
import java.awt.{BorderLayout, Dimension}
wenzelm@34748
    15
wenzelm@34424
    16
import javax.swing.{JButton, JPanel, JScrollPane}
wenzelm@34318
    17
wenzelm@34748
    18
import java.util.logging.{Logger, Level}
wenzelm@34748
    19
wenzelm@34745
    20
import org.lobobrowser.html.parser._
wenzelm@34745
    21
import org.lobobrowser.html.test._
wenzelm@34745
    22
import org.lobobrowser.html.gui._
wenzelm@34745
    23
import org.lobobrowser.html._
wenzelm@34745
    24
import org.lobobrowser.html.style.CSSUtilities
wenzelm@34745
    25
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
wenzelm@34318
    26
wenzelm@34428
    27
import org.gjt.sp.jedit.jEdit
wenzelm@34318
    28
import org.gjt.sp.jedit.View
wenzelm@34424
    29
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34428
    30
import org.gjt.sp.jedit.textarea.AntiAlias
wenzelm@34424
    31
wenzelm@34745
    32
import scala.io.Source
wenzelm@34745
    33
wenzelm@34318
    34
wenzelm@34318
    35
class StateViewDockable(view : View, position : String) extends JPanel {
wenzelm@34424
    36
wenzelm@34428
    37
  // outer panel
wenzelm@34424
    38
  if (position == DockableWindowManager.FLOATING)
wenzelm@34424
    39
    setPreferredSize(new Dimension(500, 250))
immler@34406
    40
  setLayout(new BorderLayout)
immler@34406
    41
wenzelm@34748
    42
wenzelm@34748
    43
  // global logging
wenzelm@34745
    44
  
wenzelm@34748
    45
  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
wenzelm@34748
    46
wenzelm@34748
    47
wenzelm@34745
    48
  // document template with styles
wenzelm@34428
    49
wenzelm@34745
    50
  private def try_file(name: String): String =
wenzelm@34745
    51
  {
wenzelm@34745
    52
    val file = Isabelle.system.platform_file(name)
wenzelm@34745
    53
    if (file.exists) Source.fromFile(file).mkString else ""
wenzelm@34745
    54
  }
wenzelm@34428
    55
immler@34361
    56
wenzelm@34745
    57
  // HTML panel
wenzelm@34745
    58
wenzelm@34745
    59
  val panel = new HtmlPanel
wenzelm@34745
    60
  val ucontext = new SimpleUserAgentContext
wenzelm@34745
    61
  val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
wenzelm@34745
    62
  val doc = {
wenzelm@34745
    63
    val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@34745
    64
    builder.parse(new InputSourceImpl(new StringReader(
wenzelm@34745
    65
      """<?xml version="1.0" encoding="utf-8"?>
wenzelm@34745
    66
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34745
    67
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34745
    68
<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34745
    69
<head>
wenzelm@34745
    70
<style media="all" type="text/css">
wenzelm@34745
    71
""" +
wenzelm@34745
    72
  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
wenzelm@34747
    73
"""
wenzelm@34747
    74
body {
wenzelm@34749
    75
  font-family: IsabelleText;
wenzelm@34747
    76
  font-size: 14pt;
wenzelm@34747
    77
}
wenzelm@34747
    78
""" +
wenzelm@34745
    79
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@34745
    80
"""
wenzelm@34745
    81
</style>
wenzelm@34745
    82
</head>
wenzelm@34745
    83
</html>
wenzelm@34745
    84
""")))
wenzelm@34428
    85
  }
wenzelm@34428
    86
wenzelm@34749
    87
  val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
wenzelm@34745
    88
  doc.appendChild(empty_body)
wenzelm@34428
    89
wenzelm@34745
    90
  panel.setDocument(doc, rcontext)
wenzelm@34745
    91
  add(panel, BorderLayout.CENTER)
wenzelm@34428
    92
wenzelm@34745
    93
  
immler@34669
    94
  // register for state-view
immler@34669
    95
  Isabelle.plugin.state_update += (cmd => {
immler@34669
    96
    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
wenzelm@34745
    97
wenzelm@34745
    98
    val node =
wenzelm@34745
    99
      if (cmd == null) empty_body
wenzelm@34749
   100
      else {
wenzelm@34749
   101
        val xml = XML.elem(HTML.BODY,
wenzelm@34749
   102
          cmd.results(theory_view.current_document).
wenzelm@34749
   103
            map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
wenzelm@34749
   104
        XML.document_node(doc, xml)
wenzelm@34749
   105
      }
wenzelm@34749
   106
    Swing_Thread.later {
wenzelm@34749
   107
      doc.removeChild(doc.getLastChild())
wenzelm@34749
   108
      doc.appendChild(node)
wenzelm@34749
   109
      panel.delayedRelayout(node.asInstanceOf[NodeImpl])
wenzelm@34749
   110
    }
immler@34669
   111
  })
wenzelm@34318
   112
}