1.1 --- a/src/Pure/General/scan.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -11,8 +11,9 @@
     1.4  
     1.5  signature BASIC_SCAN =
     1.6  sig
     1.7 +  type message = unit -> string
     1.8    (*error msg handler*)
     1.9 -  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
    1.10 +  val !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b
    1.11    (*apply function*)
    1.12    val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    1.13    (*alternative*)
    1.14 @@ -41,7 +42,7 @@
    1.15    val error: ('a -> 'b) -> 'a -> 'b
    1.16    val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
    1.17    val fail: 'a -> 'b
    1.18 -  val fail_with: ('a -> string) -> 'a -> 'b
    1.19 +  val fail_with: ('a -> message) -> 'a -> 'b
    1.20    val succeed: 'a -> 'b -> 'a * 'b
    1.21    val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
    1.22    val one: ('a -> bool) -> 'a list -> 'a * 'a list
    1.23 @@ -93,19 +94,21 @@
    1.24  
    1.25  (* exceptions *)
    1.26  
    1.27 +type message = unit -> string;
    1.28 +
    1.29  exception MORE of string option;        (*need more input (prompt)*)
    1.30 -exception FAIL of string option;        (*try alternatives (reason of failure)*)
    1.31 -exception ABORT of string;              (*dead end*)
    1.32 +exception FAIL of message option;       (*try alternatives (reason of failure)*)
    1.33 +exception ABORT of message;             (*dead end*)
    1.34  
    1.35  fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    1.36  fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    1.37  fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    1.38  fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    1.39 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
    1.40 +fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
    1.41  
    1.42  fun catch scan xs = scan xs
    1.43 -  handle ABORT msg => raise Fail msg
    1.44 -    | FAIL msg => raise Fail (the_default "Syntax error" msg);
    1.45 +  handle ABORT msg => raise Fail (msg ())
    1.46 +    | FAIL msg => raise Fail (case msg of NONE => "Syntax error" | SOME m => m ());
    1.47  
    1.48  
    1.49  (* scanner combinators *)
    1.50 @@ -236,7 +239,7 @@
    1.51  
    1.52  fun finite' (Stopper (mk_stopper, is_stopper)) scan (state, input) =
    1.53    let
    1.54 -    fun lost () = raise ABORT "Bad scanner: lost stopper of finite scan!";
    1.55 +    fun lost () = raise ABORT (fn () => "Bad scanner: lost stopper of finite scan!");
    1.56  
    1.57      fun stop [] = lost ()
    1.58        | stop lst =
    1.59 @@ -244,7 +247,7 @@
    1.60            in if is_stopper x then ((), xs) else lost () end;
    1.61    in
    1.62      if exists is_stopper input then
    1.63 -      raise ABORT "Stopper may not occur in input of finite scan!"
    1.64 +      raise ABORT (fn () => "Stopper may not occur in input of finite scan!")
    1.65      else (strict scan --| lift stop) (state, input @ [mk_stopper input])
    1.66    end;
    1.67