src/Tools/jEdit/src/jedit/results_dockable.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34765 63ba7f0931e2
permissions -rw-r--r--
misc modernization of names;
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@34760
    10
wenzelm@34745
    11
import isabelle.XML
wenzelm@34318
    12
wenzelm@34760
    13
import scala.swing.{BorderPanel, Component}
wenzelm@34760
    14
wenzelm@34745
    15
import java.io.StringReader
wenzelm@34424
    16
import java.awt.{BorderLayout, Dimension}
wenzelm@34424
    17
import javax.swing.{JButton, JPanel, JScrollPane}
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@34760
    35
class Results_Dockable(view : View, position : String) extends BorderPanel
wenzelm@34760
    36
{
wenzelm@34428
    37
  // outer panel
wenzelm@34760
    38
wenzelm@34424
    39
  if (position == DockableWindowManager.FLOATING)
wenzelm@34760
    40
    preferredSize = new Dimension(500, 250)
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@34760
    91
wenzelm@34760
    92
  add(Component.wrap(panel), BorderPanel.Position.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@34749
    99
    Swing_Thread.later {
wenzelm@34757
   100
      val node =
wenzelm@34757
   101
        if (cmd == null) empty_body
wenzelm@34757
   102
        else {
wenzelm@34757
   103
          val xml = XML.elem(HTML.BODY,
wenzelm@34757
   104
            cmd.results(theory_view.current_document).
wenzelm@34757
   105
              map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
wenzelm@34757
   106
          XML.document_node(doc, xml)
wenzelm@34757
   107
        }
wenzelm@34749
   108
      doc.removeChild(doc.getLastChild())
wenzelm@34749
   109
      doc.appendChild(node)
wenzelm@34749
   110
      panel.delayedRelayout(node.asInstanceOf[NodeImpl])
wenzelm@34749
   111
    }
immler@34669
   112
  })
wenzelm@34318
   113
}