tuned -- Map.empty serves as partial function;

--- a/src/Pure/library.scala	Sat Jun 18 17:30:44 2011 +0200
+++ b/src/Pure/library.scala	Sat Jun 18 17:32:13 2011 +0200
@@ -17,14 +17,6 @@
 
 object Library
 {
-  /* partial functions */
-
-  def undefined[A, B] = new PartialFunction[A, B] {
-    def apply(x: A): B = throw new NoSuchElementException("undefined")
-    def isDefinedAt(x: A) = false
-  }
-
-
   /* separate */
 
   def separate[A](s: A, list: List[A]): List[A] =

--- a/src/Tools/jEdit/src/html_panel.scala	Sat Jun 18 17:30:44 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Sat Jun 18 17:32:13 2011 +0200
@@ -61,7 +61,7 @@
 
   /* contexts and event handling */
 
-  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
+  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Map.empty
 
   private val ucontext = new SimpleUserAgentContext
   private val rcontext = new SimpleHtmlRendererContext(this, ucontext)