# HG changeset patch
# User wenzelm
# Date 1274435463 -7200
# Node ID 49559c4e85f99916c42701b846e9f0bc29639e62
# Parent  4834c31127883e98e1a96ea38cf07afbebd12533
HTML_Panel.handler as overridable method;

diff -r 4834c3112788 -r 49559c4e85f9 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:50:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 11:51:03 2010 +0200
@@ -37,10 +37,7 @@
 }
 
 
-class HTML_Panel(
-  system: Isabelle_System,
-  initial_font_size: Int,
-  handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
+class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel
 {
   /** Lobo setup **/
 
@@ -59,11 +56,15 @@
   def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
 
 
+  /* contexts and event handling */
+
+  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
+
   private val ucontext = new SimpleUserAgentContext
   private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
   {
     private def handle(event: HTML_Panel.Event): Boolean =
-      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
+      if (handler.isDefinedAt(event)) { handler(event); true }
       else false
 
     override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
diff -r 4834c3112788 -r 49559c4e85f9 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:50:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:51:03 2010 +0200
@@ -31,7 +31,7 @@
   val controls = new FlowPanel(FlowPanel.Alignment.Right)()
   add(controls.peer, BorderLayout.NORTH)
 
-  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
+  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
   add(html_panel, BorderLayout.CENTER)