src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Fri Dec 04 23:10:11 2009 +0100 (2009-12-04)
changeset 34747 b316d05a66a4
parent 34745 83b553bd3fa3
child 34748 a2ed621f5f52
permissions -rw-r--r--
tuned message markup;
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@34424
    15
import javax.swing.{JButton, JPanel, JScrollPane}
wenzelm@34318
    16
wenzelm@34745
    17
import org.lobobrowser.html.parser._
wenzelm@34745
    18
import org.lobobrowser.html.test._
wenzelm@34745
    19
import org.lobobrowser.html.gui._
wenzelm@34745
    20
import org.lobobrowser.html._
wenzelm@34745
    21
import org.lobobrowser.html.style.CSSUtilities
wenzelm@34745
    22
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
wenzelm@34318
    23
wenzelm@34428
    24
import org.gjt.sp.jedit.jEdit
wenzelm@34318
    25
import org.gjt.sp.jedit.View
wenzelm@34424
    26
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34428
    27
import org.gjt.sp.jedit.textarea.AntiAlias
wenzelm@34424
    28
wenzelm@34745
    29
import scala.io.Source
wenzelm@34745
    30
wenzelm@34318
    31
wenzelm@34318
    32
class StateViewDockable(view : View, position : String) extends JPanel {
wenzelm@34424
    33
wenzelm@34428
    34
  // outer panel
wenzelm@34424
    35
  if (position == DockableWindowManager.FLOATING)
wenzelm@34424
    36
    setPreferredSize(new Dimension(500, 250))
immler@34406
    37
  setLayout(new BorderLayout)
immler@34406
    38
wenzelm@34745
    39
  
wenzelm@34745
    40
  // document template with styles
wenzelm@34428
    41
wenzelm@34745
    42
  private def try_file(name: String): String =
wenzelm@34745
    43
  {
wenzelm@34745
    44
    val file = Isabelle.system.platform_file(name)
wenzelm@34745
    45
    if (file.exists) Source.fromFile(file).mkString else ""
wenzelm@34745
    46
  }
wenzelm@34428
    47
immler@34361
    48
wenzelm@34745
    49
  // HTML panel
wenzelm@34745
    50
wenzelm@34745
    51
  val panel = new HtmlPanel
wenzelm@34745
    52
  val ucontext = new SimpleUserAgentContext
wenzelm@34745
    53
  val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
wenzelm@34745
    54
  val doc = {
wenzelm@34745
    55
    val builder = new DocumentBuilderImpl(ucontext, rcontext)
wenzelm@34745
    56
    builder.parse(new InputSourceImpl(new StringReader(
wenzelm@34745
    57
      """<?xml version="1.0" encoding="utf-8"?>
wenzelm@34745
    58
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
wenzelm@34745
    59
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@34745
    60
<html xmlns="http://www.w3.org/1999/xhtml">
wenzelm@34745
    61
<head>
wenzelm@34745
    62
<style media="all" type="text/css">
wenzelm@34745
    63
""" +
wenzelm@34745
    64
  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
wenzelm@34747
    65
"""
wenzelm@34747
    66
body {
wenzelm@34747
    67
  white-space: pre;
wenzelm@34747
    68
  font-family: IsabelleMono;
wenzelm@34747
    69
  font-size: 14pt;
wenzelm@34747
    70
}
wenzelm@34747
    71
""" +
wenzelm@34745
    72
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@34745
    73
"""
wenzelm@34745
    74
</style>
wenzelm@34745
    75
</head>
wenzelm@34745
    76
</html>
wenzelm@34745
    77
""")))
wenzelm@34428
    78
  }
wenzelm@34428
    79
wenzelm@34747
    80
  val empty_body = XML.document_node(doc, HTML.body(Nil))
wenzelm@34745
    81
  doc.appendChild(empty_body)
wenzelm@34428
    82
wenzelm@34745
    83
  panel.setDocument(doc, rcontext)
wenzelm@34745
    84
  add(panel, BorderLayout.CENTER)
wenzelm@34428
    85
wenzelm@34745
    86
  
immler@34669
    87
  // register for state-view
immler@34669
    88
  Isabelle.plugin.state_update += (cmd => {
immler@34669
    89
    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
wenzelm@34745
    90
wenzelm@34745
    91
    val node =
wenzelm@34745
    92
      if (cmd == null) empty_body
wenzelm@34747
    93
      else XML.document_node(doc, HTML.body(
wenzelm@34747
    94
        cmd.results(theory_view.current_document).map((t: XML.Tree) => HTML.div(HTML.spans(t)))))
wenzelm@34745
    95
    doc.removeChild(doc.getLastChild())
wenzelm@34745
    96
    doc.appendChild(node)
wenzelm@34745
    97
    panel.delayedRelayout(node.asInstanceOf[NodeImpl])
immler@34669
    98
  })
wenzelm@34318
    99
}