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