# HG changeset patch
# User wenzelm
# Date 1456861898 -3600
# Node ID 7187cb7a77c5501319578c30b58ee7e9d9639a04
# Parent  39d01eaf5292cc90e52a14f3216939d00c3df0d0
clarified modules;

diff -r 39d01eaf5292 -r 7187cb7a77c5 src/Pure/General/scan.ML
--- 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 ())
diff -r 39d01eaf5292 -r 7187cb7a77c5 src/Pure/RAW/exn.ML
--- 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;
diff -r 39d01eaf5292 -r 7187cb7a77c5 src/Pure/library.ML
--- 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);