src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Sun Dec 06 20:50:07 2009 +0100 (2009-12-06)
changeset 34748 a2ed621f5f52
parent 34747 b316d05a66a4
child 34749 e377d3d6910a
permissions -rw-r--r--
reduced logging;
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@34747
    75
  white-space: pre;
wenzelm@34747
    76
  font-family: IsabelleMono;
wenzelm@34747
    77
  font-size: 14pt;
wenzelm@34747
    78
}
wenzelm@34747
    79
""" +
wenzelm@34745
    80
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
wenzelm@34745
    81
"""
wenzelm@34745
    82
</style>
wenzelm@34745
    83
</head>
wenzelm@34745
    84
</html>
wenzelm@34745
    85
""")))
wenzelm@34428
    86
  }
wenzelm@34428
    87
wenzelm@34747
    88
  val empty_body = XML.document_node(doc, HTML.body(Nil))
wenzelm@34745
    89
  doc.appendChild(empty_body)
wenzelm@34428
    90
wenzelm@34745
    91
  panel.setDocument(doc, rcontext)
wenzelm@34745
    92
  add(panel, BorderLayout.CENTER)
wenzelm@34428
    93
wenzelm@34745
    94
  
immler@34669
    95
  // register for state-view
immler@34669
    96
  Isabelle.plugin.state_update += (cmd => {
immler@34669
    97
    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
wenzelm@34745
    98
wenzelm@34745
    99
    val node =
wenzelm@34745
   100
      if (cmd == null) empty_body
wenzelm@34747
   101
      else XML.document_node(doc, HTML.body(
wenzelm@34747
   102
        cmd.results(theory_view.current_document).map((t: XML.Tree) => HTML.div(HTML.spans(t)))))
wenzelm@34745
   103
    doc.removeChild(doc.getLastChild())
wenzelm@34745
   104
    doc.appendChild(node)
wenzelm@34745
   105
    panel.delayedRelayout(node.asInstanceOf[NodeImpl])
immler@34669
   106
  })
wenzelm@34318
   107
}