# HG changeset patch # User wenzelm # Date 1260299648 -3600 # Node ID 63ba7f0931e2e052585986a6ce61fe8cc8eaa282 # Parent 581e919c8730969a523b5b211dc3a380d2070cdf generic HTML_Panel -- specific Results_Dockable; diff -r 581e919c8730 -r 63ba7f0931e2 src/Tools/jEdit/src/jedit/results_dockable.scala --- 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( - """ - - - - - - -"""))) - } + 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) }) } diff -r 581e919c8730 -r 63ba7f0931e2 src/Tools/jEdit/src/proofdocument/html_panel.scala --- /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 = + """ + + + + + + + +""" + + + /* 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) } +}