# HG changeset patch # User wenzelm # Date 1137255254 -3600 # Node ID 3020496cff28045af3aeb845331d7a4c82746878 # Parent 677e2bdd75f00323d132fcc9b4909564d5c62cac added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all; added transform_failure; added prefix; diff -r 677e2bdd75f0 -r 3020496cff28 src/Pure/library.ML --- a/src/Pure/library.ML Sat Jan 14 17:14:13 2006 +0100 +++ b/src/Pure/library.ML Sat Jan 14 17:14:14 2006 +0100 @@ -53,16 +53,27 @@ val is_none: 'a option -> bool val perhaps: ('a -> 'a option) -> 'a -> 'a - exception EXCEPTION of exn * string - exception ERROR + (*exceptions*) val try: ('a -> 'b) -> 'a -> 'b option val can: ('a -> 'b) -> 'a -> bool + exception EXCEPTION of exn * string + val do_transform_failure: bool ref + val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b datatype 'a result = Result of 'a | Exn of exn val capture: ('a -> 'b) -> 'a -> 'b result val release: 'a result -> 'a val get_result: 'a result -> 'a option val get_exn: 'a result -> exn option + (*errors*) + exception ERROR of string + val error: string -> 'a + val cat_error: string -> string -> 'a + val sys_error: string -> 'a + val assert: bool -> string -> unit + val deny: bool -> string -> unit + val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit + (*pairs*) val pair: 'a -> 'b -> 'a * 'b val rpair: 'a -> 'b -> 'b * 'a @@ -164,9 +175,10 @@ val split_lines: string -> string list val prefix_lines: string -> string -> string val untabify: string list -> string list + val prefix: string -> string -> string val suffix: string -> string -> string + val unprefix: string -> string -> string val unsuffix: string -> string -> string - val unprefix: string -> string -> string val replicate_string: int -> string -> string val translate_string: (string -> string) -> string -> string @@ -348,12 +360,18 @@ (* exceptions *) +val do_transform_failure = ref true; + +fun transform_failure exn f x = + if ! do_transform_failure then + f x handle Interrupt => raise Interrupt | e => raise exn e + else f x; + exception EXCEPTION of exn * string; -exception ERROR; fun try f x = SOME (f x) - handle Interrupt => raise Interrupt | ERROR => raise ERROR | _ => NONE; + handle Interrupt => raise Interrupt | _ => NONE; fun can f x = is_some (try f x); @@ -374,6 +392,27 @@ | get_exn _ = NONE; +(* errors *) + +exception ERROR of string; + +fun error msg = raise ERROR msg; + +fun cat_error "" msg = error msg + | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2); + +fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg); + +fun assert p msg = if p then () else error msg; +fun deny p msg = if p then error msg else (); + +fun assert_all pred list msg = + let + fun ass [] = () + | ass (x :: xs) = if pred x then ass xs else error (msg x); + in ass list end; + + (** pairs **) @@ -848,16 +887,17 @@ else flat (#2 (foldl_map untab (0, chs))) end; +fun prefix prfx s = prfx ^ s; fun suffix sffx s = s ^ sffx; +fun unprefix prfx s = + if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx) + else raise Fail "unprefix"; + fun unsuffix sffx s = if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx) else raise Fail "unsuffix"; -fun unprefix prfx s = - if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx) - else raise Fail "unprefix"; - fun replicate_string 0 _ = "" | replicate_string 1 a = a | replicate_string k a =