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