--- a/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 20:13:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 20:14:08 2009 +0100
@@ -1,38 +1,25 @@
/*
- * Dockable window with rendered state output
+ * Dockable window with result message output
*
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
+ * @author Makarius
*/
package isabelle.jedit
-import isabelle.XML
+import isabelle.proofdocument.HTML_Panel
+import scala.io.Source
import scala.swing.{BorderPanel, Component}
-import java.io.StringReader
-import java.awt.{BorderLayout, Dimension}
-import javax.swing.{JButton, JPanel, JScrollPane}
-import java.util.logging.{Logger, Level}
+import java.awt.Dimension
-import org.lobobrowser.html.parser._
-import org.lobobrowser.html.test._
-import org.lobobrowser.html.gui._
-import org.lobobrowser.html._
-import org.lobobrowser.html.style.CSSUtilities
-import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
-
-import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.textarea.AntiAlias
-
-import scala.io.Source
-class Results_Dockable(view : View, position : String) extends BorderPanel
+
+class Results_Dockable(view: View, position: String) extends BorderPanel
{
// outer panel
@@ -40,74 +27,16 @@
preferredSize = new Dimension(500, 250)
- // global logging
-
- Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
-
- // document template with styles
-
- private def try_file(name: String): String =
- {
- val file = Isabelle.system.platform_file(name)
- if (file.exists) Source.fromFile(file).mkString else ""
- }
-
-
// HTML panel
- val panel = new HtmlPanel
- val ucontext = new SimpleUserAgentContext
- val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
- val doc = {
- val builder = new DocumentBuilderImpl(ucontext, rcontext)
- builder.parse(new InputSourceImpl(new StringReader(
- """<?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
- "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
-<style media="all" type="text/css">
-""" +
- try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
-"""
-body {
- font-family: IsabelleText;
- font-size: 14pt;
-}
-""" +
- try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
-"""
-</style>
-</head>
-</html>
-""")))
- }
+ val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
+ add(Component.wrap(html_panel), BorderPanel.Position.Center)
- val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
- doc.appendChild(empty_body)
-
- panel.setDocument(doc, rcontext)
-
- add(Component.wrap(panel), BorderPanel.Position.Center)
-
-
- // register for state-view
Isabelle.plugin.state_update += (cmd => {
val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
-
- Swing_Thread.later {
- val node =
- if (cmd == null) empty_body
- else {
- val xml = XML.elem(HTML.BODY,
- cmd.results(theory_view.current_document).
- map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
- XML.document_node(doc, xml)
- }
- doc.removeChild(doc.getLastChild())
- doc.appendChild(node)
- panel.delayedRelayout(node.asInstanceOf[NodeImpl])
- }
+ val body =
+ if (cmd == null) Nil // FIXME ??
+ else cmd.results(theory_view.current_document)
+ html_panel.render(body)
})
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Tue Dec 08 20:14:08 2009 +0100
@@ -0,0 +1,104 @@
+/*
+ * HTML panel based on Lobo/Cobra
+ *
+ * @author Makarius
+ */
+
+package isabelle.proofdocument
+
+
+import java.io.StringReader
+import java.awt.{BorderLayout, Dimension}
+import javax.swing.{JButton, JPanel, JScrollPane}
+import java.util.logging.{Logger, Level}
+
+import org.w3c.dom.Document
+
+import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
+import org.lobobrowser.html.gui.HtmlPanel
+import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
+import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
+
+import scala.io.Source
+import scala.actors.Actor._
+
+
+class HTML_Panel(sys: Isabelle_System, initial_font_size: Int) extends HtmlPanel
+{
+ // global logging
+ Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
+
+
+ /* document template */
+
+ private def try_file(name: String): String =
+ {
+ val file = sys.platform_file(name)
+ if (file.exists) Source.fromFile(file).mkString else ""
+ }
+
+ private def template(font_size: Int): String =
+ """<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<style media="all" type="text/css">""" +
+ try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+ "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }\n" +
+ try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+
+
+ /* actor with local state */
+
+ private val ucontext = new SimpleUserAgentContext
+ private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
+ private val builder = new DocumentBuilderImpl(ucontext, rcontext)
+
+ private case class Init(font_size: Int)
+ private case class Render(body: List[XML.Tree])
+
+ private val main_actor = actor {
+ // double buffering
+ var doc1: Document = null
+ var doc2: Document = null
+
+ loop {
+ react {
+ case Init(font_size) =>
+ val src = template(font_size)
+ def parse() = builder.parse(new InputSourceImpl(new StringReader(src)))
+ doc1 = parse()
+ doc2 = parse()
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case Render(body) =>
+ val doc = doc2
+ val node =
+ XML.document_node(doc,
+ XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
+ doc.removeChild(doc.getLastChild())
+ doc.appendChild(node)
+ doc2 = doc1
+ doc1 = doc
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case bad => System.err.println("prover: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ main_actor ! Init(initial_font_size)
+
+
+ /* main method wrappers */
+
+ def init(font_size: Int) { main_actor ! Init(font_size) }
+ def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+}