src/Tools/jEdit/src/html_panel.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 43442 e1fff67b23ac
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 42976
diff changeset
     1
/*  Title:      Tools/jEdit/src/html_panel.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36735
diff changeset
     2
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36735
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 36735
diff changeset
     4
HTML panel based on Lobo/Cobra.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36735
diff changeset
     5
*/
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     6
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34823
diff changeset
     7
package isabelle.jedit
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     8
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
     9
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    11
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    12
import java.io.StringReader
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    13
import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
34775
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    14
import java.awt.event.MouseEvent
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    15
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    16
import java.util.logging.{Logger, Level}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    17
34775
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    18
import org.w3c.dom.html2.HTMLElement
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    19
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    20
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    21
import org.lobobrowser.html.gui.HtmlPanel
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    22
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    23
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    24
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    25
import scala.actors.Actor._
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    26
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    27
34775
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    28
object HTML_Panel
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    29
{
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    30
  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    31
  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    32
  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    33
  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    34
  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    35
  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    36
}
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    37
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
    38
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    39
class HTML_Panel(
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    40
    system: Isabelle_System,
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    41
    initial_font_family: String,
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    42
    initial_font_size: Int)
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
    43
  extends HtmlPanel
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    44
{
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
    45
  /** Lobo setup **/
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
    46
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
    47
  /* global logging */
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
    48
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    49
  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    50
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    51
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
    52
  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
36817
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    53
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    54
  val screen_resolution =
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    55
    if (GraphicsEnvironment.isHeadless()) 72
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    56
    else Toolkit.getDefaultToolkit().getScreenResolution()
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    57
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    58
  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    59
  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    60
ed97e877ff2d more precise pretty printing based on actual font metrics;
wenzelm
parents: 36814
diff changeset
    61
37036
49559c4e85f9 HTML_Panel.handler as overridable method;
wenzelm
parents: 37034
diff changeset
    62
  /* contexts and event handling */
49559c4e85f9 HTML_Panel.handler as overridable method;
wenzelm
parents: 37034
diff changeset
    63
49559c4e85f9 HTML_Panel.handler as overridable method;
wenzelm
parents: 37034
diff changeset
    64
  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
49559c4e85f9 HTML_Panel.handler as overridable method;
wenzelm
parents: 37034
diff changeset
    65
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    66
  private val ucontext = new SimpleUserAgentContext
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    67
  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    68
  {
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    69
    private def handle(event: HTML_Panel.Event): Boolean =
42976
9901f877eeb7 invert event propagation flag -- in lobobrowser api, true means re-propagate
krauss
parents: 39740
diff changeset
    70
      if (handler.isDefinedAt(event)) { handler(event); false }
9901f877eeb7 invert event propagation flag -- in lobobrowser api, true means re-propagate
krauss
parents: 39740
diff changeset
    71
      else true
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    72
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    73
    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    74
      handle(HTML_Panel.Context_Menu(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    75
    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    76
      handle(HTML_Panel.Mouse_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    77
    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    78
      handle(HTML_Panel.Double_Click(elem, event))
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    79
    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    80
      { handle(HTML_Panel.Mouse_Over(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    81
    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    82
      { handle(HTML_Panel.Mouse_Out(elem, event)) }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    83
  }
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    84
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    85
  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    86
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
    87
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
    88
  /* document template with style sheets */
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    89
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
    90
  private val template_head =
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    91
    """<?xml version="1.0" encoding="utf-8"?>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    92
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    93
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    94
<html xmlns="http://www.w3.org/1999/xhtml">
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
    95
<head>
34770
0c630c52fc74 prefer options from running application;
wenzelm
parents: 34769
diff changeset
    96
<style media="all" type="text/css">
0c630c52fc74 prefer options from running application;
wenzelm
parents: 34769
diff changeset
    97
""" +
37058
c47653f3ec14 rendering information and style sheets via settings;
wenzelm
parents: 37040
diff changeset
    98
  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
    99
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   100
  private val template_tail =
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   101
"""
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   102
</style>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   103
</head>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   104
<body/>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   105
</html>
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   106
"""
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   107
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   108
  private def template(font_family: String, font_size: Int): String =
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   109
    template_head +
37202
wenzelm
parents: 37164
diff changeset
   110
    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
37015
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   111
    template_tail
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   112
39207774a9b7 read style sheets only once;
wenzelm
parents: 37014
diff changeset
   113
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   114
  /** main actor **/
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   115
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   116
  /* internal messages */
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   117
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   118
  private case class Resize(font_family: String, font_size: Int)
39590
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   119
  private case class Render_Document(text: String)
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
   120
  private case class Render(body: XML.Body)
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39590
diff changeset
   121
  private case class Render_Sync(body: XML.Body)
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   122
  private case object Refresh
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   123
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   124
  private val main_actor = actor {
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   125
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   126
    /* internal state */
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   127
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   128
    var current_font_metrics: FontMetrics = null
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   129
    var current_font_family = ""
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   130
    var current_font_size: Int = 0
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   131
    var current_margin: Int = 0
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
   132
    var current_body: XML.Body = Nil
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   133
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   134
    def resize(font_family: String, font_size: Int)
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   135
    {
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   136
      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   137
      val (font_metrics, margin) =
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   138
        Swing_Thread.now {
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   139
          val metrics = getFontMetrics(font)
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   140
          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   141
        }
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   142
      if (current_font_metrics == null ||
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   143
          current_font_family != font_family ||
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   144
          current_font_size != font_size ||
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   145
          current_margin != margin)
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   146
      {
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   147
        current_font_metrics = font_metrics
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   148
        current_font_family = font_family
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   149
        current_font_size = font_size
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   150
        current_margin = margin
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36995
diff changeset
   151
        refresh()
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   152
      }
36814
dc85664dbf6d support Isabelle plugin properties with defaults;
wenzelm
parents: 36790
diff changeset
   153
    }
dc85664dbf6d support Isabelle plugin properties with defaults;
wenzelm
parents: 36790
diff changeset
   154
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36995
diff changeset
   155
    def refresh() { render(current_body) }
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36995
diff changeset
   156
39590
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   157
    def render_document(text: String)
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   158
    {
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   159
      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   160
      Swing_Thread.later { setDocument(doc, rcontext) }
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   161
    }
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   162
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
   163
    def render(body: XML.Body)
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   164
    {
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   165
      current_body = body
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   166
      val html_body =
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   167
        current_body.flatMap(div =>
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   168
          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
38235
25d6f789618b fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
wenzelm
parents: 37202
diff changeset
   169
            .map(t =>
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38235
diff changeset
   170
              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38235
diff changeset
   171
                HTML.spans(t, true))))
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   172
      val doc =
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   173
        builder.parse(
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   174
          new InputSourceImpl(
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   175
            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   176
      doc.removeChild(doc.getLastChild())
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   177
      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   178
      Swing_Thread.later { setDocument(doc, rcontext) }
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   179
    }
34775
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
   180
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   181
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   182
    /* main loop */
36993
b7cce32953f0 more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents: 36992
diff changeset
   183
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   184
    resize(initial_font_family, initial_font_size)
34775
49245d68f7e4 basic setup for HTML_Panel event handling;
wenzelm
parents: 34770
diff changeset
   185
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   186
    loop {
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   187
      react {
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   188
        case Resize(font_family, font_size) => resize(font_family, font_size)
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   189
        case Refresh => refresh()
39590
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   190
        case Render_Document(text) => render_document(text)
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   191
        case Render(body) => render(body)
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39590
diff changeset
   192
        case Render_Sync(body) => render(body); reply(())
34769
826525fc5285 more precise messages;
wenzelm
parents: 34766
diff changeset
   193
        case bad => System.err.println("main_actor: ignoring bad message " + bad)
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   194
      }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   195
    }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   196
  }
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   197
37034
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   198
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   199
  /* external methods */
9640f6546179 more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
wenzelm
parents: 37016
diff changeset
   200
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37069
diff changeset
   201
  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36995
diff changeset
   202
  def refresh() { main_actor ! Refresh }
39590
2258769f112f basic support for full document rendering;
wenzelm
parents: 38573
diff changeset
   203
  def render_document(text: String) { main_actor ! Render_Document(text) }
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
   204
  def render(body: XML.Body) { main_actor ! Render(body) }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39590
diff changeset
   205
  def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents:
diff changeset
   206
}