# HG changeset patch # User wenzelm # Date 1259943284 -3600 # Node ID 83b553bd3fa30edd478467b21ecfbec01ce876fe # Parent 30fba76e6cc22bc34c2a77d11ba2028fa8615a57 basic setup for Cobra HTML renderer; diff -r 30fba76e6cc2 -r 83b553bd3fa3 src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Fri Dec 04 17:14:16 2009 +0100 +++ b/src/Tools/jEdit/README_BUILD Fri Dec 04 17:14:44 2009 +0100 @@ -27,6 +27,11 @@ https://xhtmlrenderer.dev.java.net/ Netbeans Library "Flying-Saucer" = .../core-renderer.jar +* Cobra Renderer + http://lobobrowser.org/cobra.jsp + Netbeans Library "Cobra-Renderer" = .../cobra.jar + Netbenas Library "Rhino-JavaScript" = .../js.jar + * Isabelle/Pure Scala components Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar diff -r 30fba76e6cc2 -r 83b553bd3fa3 src/Tools/jEdit/nbproject/project.properties --- a/src/Tools/jEdit/nbproject/project.properties Fri Dec 04 17:14:16 2009 +0100 +++ b/src/Tools/jEdit/nbproject/project.properties Fri Dec 04 17:14:44 2009 +0100 @@ -35,7 +35,9 @@ ${libs.Isabelle-Pure.classpath}:\ ${libs.Sidekick.classpath}:\ ${libs.ErrorList.classpath}:\ - ${libs.Hyperlink.classpath} + ${libs.Hyperlink.classpath}:\ + ${libs.Cobra-Renderer.classpath}:\ + ${libs.Rhino-JavaScript.classpath} # Space-separated list of extra javac options javac.compilerargs= javac.deprecation=false diff -r 30fba76e6cc2 -r 83b553bd3fa3 src/Tools/jEdit/src/jedit/StateViewDockable.scala --- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Fri Dec 04 17:14:16 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Fri Dec 04 17:14:44 2009 +0100 @@ -7,23 +7,27 @@ package isabelle.jedit +import isabelle.renderer.UserAgent +import isabelle.XML +import java.io.StringReader import java.awt.{BorderLayout, Dimension} import javax.swing.{JButton, JPanel, JScrollPane} -import isabelle.renderer.UserAgent - -import org.xhtmlrenderer.simple.{XHTMLPanel, FSScrollPane} -import org.xhtmlrenderer.context.AWTFontResolver -import org.xhtmlrenderer.layout.SharedContext; -import org.xhtmlrenderer.extend.TextRenderer; -import org.xhtmlrenderer.swing.Java2DTextRenderer; +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 StateViewDockable(view : View, position : String) extends JPanel { @@ -32,53 +36,57 @@ setPreferredSize(new Dimension(500, 250)) setLayout(new BorderLayout) + + // document template with styles - // XHTML panel - val panel = new XHTMLPanel(new UserAgent) + private def try_file(name: String): String = + { + val file = Isabelle.system.platform_file(name) + if (file.exists) Source.fromFile(file).mkString else "" + } - // anti-aliasing - // TODO: proper EditBus event handling - { - val aa = jEdit.getProperty("view.antiAlias") - if (aa != null && aa != AntiAlias.NONE) { - panel.getSharedContext.setTextRenderer( - { - val renderer = new Java2DTextRenderer - renderer.setSmoothingThreshold(0) - renderer - }) - } + // 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( + """ + + + + + + +"""))) } - - // copy & paste - (new SelectionActions).install(panel) + val empty_body = XML.document_node(doc, XML.Elem("body", Nil, List(XML.Text("empty")))) + doc.appendChild(empty_body) + panel.setDocument(doc, rcontext) + add(panel, BorderLayout.CENTER) - // scrolling - add(new FSScrollPane(panel), BorderLayout.CENTER) - + // register for state-view Isabelle.plugin.state_update += (cmd => { val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view - if (cmd == null) - panel.setDocument(null: org.w3c.dom.Document) - else - panel.setDocument(cmd.result_document(theory_view.current_document()), - UserAgent.base_URL) + + val node = + if (cmd == null) empty_body + else XML.document_node(doc, XML.Elem("body", Nil, List(XML.Text(XML.content( + cmd.results(theory_view.current_document)).mkString)))) + doc.removeChild(doc.getLastChild()) + doc.appendChild(node) + panel.delayedRelayout(node.asInstanceOf[NodeImpl]) }) - - private val fontResolver = - panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] - if (Isabelle.plugin.font != null) - fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font) - - Isabelle.plugin.font_changed += (font => { - if (Isabelle.plugin.font != null) - fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font) - - panel.relayout() - }) - }