--- a/src/Pure/General/scan.ML Tue Mar 01 19:42:59 2016 +0100
+++ b/src/Pure/General/scan.ML Tue Mar 01 20:51:38 2016 +0100
@@ -109,7 +109,7 @@
fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE;
fun strict scan xs = scan xs handle MORE () => raise FAIL NONE;
-fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
+fun error scan xs = scan xs handle ABORT msg => Exn.error (msg ());
fun catch scan xs = scan xs
handle ABORT msg => raise Fail (msg ())
--- a/src/Pure/RAW/exn.ML Tue Mar 01 19:42:59 2016 +0100
+++ b/src/Pure/RAW/exn.ML Tue Mar 01 20:51:38 2016 +0100
@@ -4,8 +4,16 @@
Support for exceptions.
*)
+signature BASIC_EXN =
+sig
+ exception ERROR of string
+ val error: string -> 'a
+ val cat_error: string -> string -> 'a
+end;
+
signature EXN =
sig
+ include BASIC_EXN
datatype 'a result = Res of 'a | Exn of exn
val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
@@ -86,6 +94,20 @@
exception EXCEPTIONS of exn list;
+
+(* user errors *)
+
+exception ERROR of string;
+
+fun error msg = raise ERROR msg;
+
+fun cat_error "" msg = error msg
+ | cat_error msg "" = error msg
+ | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
+
end;
datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
--- a/src/Pure/library.ML Tue Mar 01 19:42:59 2016 +0100
+++ b/src/Pure/library.ML Tue Mar 01 20:51:38 2016 +0100
@@ -28,11 +28,6 @@
val funpow: int -> ('a -> 'a) -> 'a -> 'a
val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- (*user errors*)
- exception ERROR of string
- val error: string -> 'a
- val cat_error: string -> string -> 'a
-
(*pairs*)
val pair: 'a -> 'b -> 'a * 'b
val rpair: 'a -> 'b -> 'b * 'a
@@ -252,16 +247,6 @@
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
-(* user errors *)
-
-exception ERROR of string;
-fun error msg = raise ERROR msg;
-
-fun cat_error "" msg = error msg
- | cat_error msg "" = error msg
- | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
-
-
(* pairs *)
fun pair x y = (x, y);