--- 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)