# HG changeset patch
# User wenzelm
# Date 931635241 -7200
# Node ID d33b1629eaf9b052c57a4c00ad96002a216f80cb
# Parent  2ed4b761d6d59d50d53a8d2e8a080fca18bd1eea
try/can: pass Interrupt and ERROR;
nth_elem_string: use try;

diff -r 2ed4b761d6d5 -r d33b1629eaf9 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jul 09 19:11:50 1999 +0200
+++ b/src/Pure/library.ML	Sat Jul 10 21:34:01 1999 +0200
@@ -41,8 +41,8 @@
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
   val apsome: ('a -> 'b) -> 'a option -> 'b option
+  val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool
-  val try: ('a -> 'b) -> 'a -> 'b option
 
   (*pairs*)
   val pair: 'a -> 'b -> 'a * 'b
@@ -316,9 +316,15 @@
 fun apsome f (Some x) = Some (f x)
   | apsome _ None = None;
 
-(*handle partial functions*)
-fun can f x = (f x; true) handle _ => false;
-fun try f x = Some (f x) handle _ => None;
+
+(* exception handling *)
+
+exception ERROR;
+
+fun try f x = Some (f x)
+  handle Interrupt => raise Interrupt | ERROR => raise ERROR | _ => None;
+
+fun can f x = is_some (try f x);
 
 
 
@@ -662,7 +668,9 @@
 (*functions tuned for strings, avoiding explode*)
 
 fun nth_elem_string (i, str) =
-  String.substring (str, i, 1) handle _ => raise LIST "nth_elem_string";
+  (case try String.substring (str, i, 1) of
+    Some s => s
+  | None => raise LIST "nth_elem_string");
 
 fun foldl_string f (x0, str) =
   let
@@ -1077,7 +1085,7 @@
 fun warning s = ! warning_fn s;
 
 (*print error message and abort to top level*)
-exception ERROR;
+
 fun error_msg s = ! error_fn s;
 fun error s = (error_msg s; raise ERROR);
 fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);