# HG changeset patch
# User wenzelm
# Date 1308411133 -7200
# Node ID e1fff67b23ac5f463ed5182d65003be51ee61167
# Parent  39efc484bc9800a5423f904f9ec53baa63e2616b
tuned -- Map.empty serves as partial function;

diff -r 39efc484bc98 -r e1fff67b23ac src/Pure/library.scala
--- 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] =
diff -r 39efc484bc98 -r e1fff67b23ac src/Tools/jEdit/src/html_panel.scala
--- 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)