1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:50:19 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:51:03 2010 +0200
     1.3 @@ -37,10 +37,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class HTML_Panel(
     1.8 -  system: Isabelle_System,
     1.9 -  initial_font_size: Int,
    1.10 -  handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
    1.11 +class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel
    1.12  {
    1.13    /** Lobo setup **/
    1.14  
    1.15 @@ -59,11 +56,15 @@
    1.16    def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
    1.17  
    1.18  
    1.19 +  /* contexts and event handling */
    1.20 +
    1.21 +  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
    1.22 +
    1.23    private val ucontext = new SimpleUserAgentContext
    1.24    private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    1.25    {
    1.26      private def handle(event: HTML_Panel.Event): Boolean =
    1.27 -      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
    1.28 +      if (handler.isDefinedAt(event)) { handler(event); true }
    1.29        else false
    1.30  
    1.31      override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =

     2.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:50:19 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:51:03 2010 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4    val controls = new FlowPanel(FlowPanel.Alignment.Right)()
     2.5    add(controls.peer, BorderLayout.NORTH)
     2.6  
     2.7 -  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
     2.8 +  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
     2.9    add(html_panel, BorderLayout.CENTER)
    2.10  
    2.11