# HG changeset patch
# User wenzelm
# Date 1274435419 -7200
# Node ID 4834c31127883e98e1a96ea38cf07afbebd12533
# Parent  9640f654617907e1bc85f6945dd6863a71461802
added Library.undefined (in Scala);

diff -r 9640f6546179 -r 4834c3112788 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri May 21 11:16:01 2010 +0200
+++ b/src/Pure/library.scala	Fri May 21 11:50:19 2010 +0200
@@ -17,6 +17,14 @@
 
 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] =