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