src/Tools/jEdit/src/proofdocument/html_panel.scala
author wenzelm
Tue, 08 Dec 2009 22:38:32 +0100
changeset 34770 0c630c52fc74
parent 34769 826525fc5285
child 34775 49245d68f7e4
permissions -rw-r--r--
prefer options from running application;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     1
/*
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     2
 * HTML panel based on Lobo/Cobra
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     3
 *
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     4
 * @author Makarius
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     5
 */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     6
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     7
package isabelle.proofdocument
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     8
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     9
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    10
import java.io.StringReader
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    11
import java.awt.{BorderLayout, Dimension}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    12
import javax.swing.{JButton, JPanel, JScrollPane}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    13
import java.util.logging.{Logger, Level}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    14
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    15
import org.w3c.dom.Document
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    16
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    17
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    18
import org.lobobrowser.html.gui.HtmlPanel
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    19
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    20
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    21
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    22
import scala.io.Source
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    23
import scala.actors.Actor._
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    24
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    25
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    26
class HTML_Panel(sys: Isabelle_System, initial_font_size: Int) extends HtmlPanel
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    27
{
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    28
  // global logging
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    29
  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    30
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    31
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    32
  /* document template */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    33
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    34
  private def try_file(name: String): String =
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    35
  {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    36
    val file = sys.platform_file(name)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    37
    if (file.exists) Source.fromFile(file).mkString else ""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    38
  }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    39
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    40
  private def template(font_size: Int): String =
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    41
    """<?xml version="1.0" encoding="utf-8"?>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    42
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    43
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    44
<html xmlns="http://www.w3.org/1999/xhtml">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    45
<head>
34770
0c630c52fc74 prefer options from running application;
wenzelm
parents: 34769
diff changeset
    46
<style media="all" type="text/css">
0c630c52fc74 prefer options from running application;
wenzelm
parents: 34769
diff changeset
    47
""" +
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    48
  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    49
  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
34770
0c630c52fc74 prefer options from running application;
wenzelm
parents: 34769
diff changeset
    50
  "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    51
"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    52
</style>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    53
</head>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    54
<body/>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    55
</html>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    56
"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    57
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    58
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    59
  /* actor with local state */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    60
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    61
  private val ucontext = new SimpleUserAgentContext
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    62
  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    63
  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    64
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    65
  private case class Init(font_size: Int)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    66
  private case class Render(body: List[XML.Tree])
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    67
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    68
  private val main_actor = actor {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    69
    // double buffering
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    70
    var doc1: Document = null
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    71
    var doc2: Document = null
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    72
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    73
    loop {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    74
      react {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    75
        case Init(font_size) =>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    76
          val src = template(font_size)
34766
4f9bcd4b5bd1 provide dummy URL;
wenzelm
parents: 34765
diff changeset
    77
          def parse() =
4f9bcd4b5bd1 provide dummy URL;
wenzelm
parents: 34765
diff changeset
    78
            builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    79
          doc1 = parse()
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    80
          doc2 = parse()
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    81
          Swing_Thread.now { setDocument(doc1, rcontext) }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    82
          
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    83
        case Render(body) =>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    84
          val doc = doc2
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    85
          val node =
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    86
            XML.document_node(doc,
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    87
              XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    88
          doc.removeChild(doc.getLastChild())
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    89
          doc.appendChild(node)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    90
          doc2 = doc1
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    91
          doc1 = doc
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    92
          Swing_Thread.now { setDocument(doc1, rcontext) }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    93
34769
826525fc5285 more precise messages;
wenzelm
parents: 34766
diff changeset
    94
        case bad => System.err.println("main_actor: ignoring bad message " + bad)
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    95
      }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    96
    }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    97
  }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    98
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    99
  main_actor ! Init(initial_font_size)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   100
  
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   101
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   102
  /* main method wrappers */
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   103
  
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   104
  def init(font_size: Int) { main_actor ! Init(font_size) }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   105
  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   106
}