1.1 --- a/src/Pure/library.scala	Sat Jun 18 17:30:44 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Sat Jun 18 17:32:13 2011 +0200
     1.3 @@ -17,14 +17,6 @@
     1.4  
     1.5  object Library
     1.6  {
     1.7 -  /* partial functions */
     1.8 -
     1.9 -  def undefined[A, B] = new PartialFunction[A, B] {
    1.10 -    def apply(x: A): B = throw new NoSuchElementException("undefined")
    1.11 -    def isDefinedAt(x: A) = false
    1.12 -  }
    1.13 -
    1.14 -
    1.15    /* separate */
    1.16  
    1.17    def separate[A](s: A, list: List[A]): List[A] =

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