src/Tools/jEdit/src/proofdocument/html_panel.scala
changeset 34765 63ba7f0931e2
child 34766 4f9bcd4b5bd1
--- /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) }
+}