1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -331,18 +331,19 @@
     1.4  
     1.5  fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
     1.6  
     1.7 -fun scan_err msg [] = "Boogie (at end of input): " ^ msg
     1.8 -  | scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^
     1.9 -      msg
    1.10 +fun scan_err msg [] = (fn () => "Boogie (at end of input): " ^ msg ())
    1.11 +  | scan_err msg ((i, _) :: _) =
    1.12 +      (fn () => "Boogie (at line " ^ string_of_int i ^ "): " ^ msg ())
    1.13  
    1.14 -fun scan_fail msg = Scan.fail_with (scan_err msg)
    1.15 +fun scan_fail' msg = Scan.fail_with (scan_err msg)
    1.16 +fun scan_fail s = scan_fail' (fn () => s)
    1.17  
    1.18  fun finite scan fold_lines input =
    1.19    let val (i, ts) = tokenize fold_lines input
    1.20    in
    1.21      (case Scan.error (Scan.finite (stopper i) scan) ts of
    1.22        (x, []) => x
    1.23 -    | (_, ts') => error (scan_err "unparsed input" ts'))
    1.24 +    | (_, ts') => error ((scan_err (fn () => "unparsed input") ts') ()))
    1.25    end
    1.26  
    1.27  fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
    1.28 @@ -361,7 +362,7 @@
    1.29  fun scan_lookup kind tab key =
    1.30    (case Symtab.lookup tab key of
    1.31      SOME value => Scan.succeed value
    1.32 -  | NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key))
    1.33 +  | NONE => scan_fail' (fn () => "undefined " ^ kind ^ ": " ^ quote key))
    1.34  
    1.35  fun typ tds =
    1.36    let

     2.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jul 23 16:12:12 2011 +0200
     2.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jul 23 16:37:17 2011 +0200
     2.3 @@ -194,9 +194,9 @@
     2.4      fun get_pos [] = " (past end-of-text!)"
     2.5        | get_pos ((_, pos) :: _) = Position.str_of pos;
     2.6  
     2.7 -    fun err (syms, msg) =
     2.8 +    fun err (syms, msg) = fn () =>
     2.9        text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
    2.10 -      (case msg of NONE => "" | SOME s => "\n" ^ s);
    2.11 +        (case msg of NONE => "" | SOME m => "\n" ^ m ());
    2.12    in Scan.!! err scan end;
    2.13  
    2.14  val any_line' =

     3.1 --- a/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:12:12 2011 +0200
     3.2 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:37:17 2011 +0200
     3.3 @@ -72,10 +72,10 @@
     3.4      fun get_pos [] = " (past end-of-file!)"
     3.5        | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
     3.6  
     3.7 -    fun err (syms, msg) =
     3.8 +    fun err (syms, msg) = fn () =>
     3.9        "Syntax error" ^ get_pos syms ^ " at " ^
    3.10 -      beginning 10 (map Fdl_Lexer.unparse syms) ^
    3.11 -      (case msg of NONE => "" | SOME s => "\n" ^ s ^ " expected");
    3.12 +        beginning 10 (map Fdl_Lexer.unparse syms) ^
    3.13 +        (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected");
    3.14    in Scan.!! err scan end;
    3.15  
    3.16  fun parse_all p =
    3.17 @@ -84,7 +84,7 @@
    3.18  
    3.19  (** parsers **)
    3.20  
    3.21 -fun group s p = p || Scan.fail_with (K s);
    3.22 +fun group s p = p || Scan.fail_with (K (fn () => s));
    3.23  
    3.24  fun $$$ s = group s
    3.25    (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso

     4.1 --- a/src/Pure/General/antiquote.ML	Sat Jul 23 16:12:12 2011 +0200
     4.2 +++ b/src/Pure/General/antiquote.ML	Sat Jul 23 16:37:17 2011 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4  
     4.5  val scan_antiq =
     4.6    Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     4.7 -    Symbol_Pos.!!! "missing closing brace of antiquotation"
     4.8 +    Symbol_Pos.!!! (fn () => "missing closing brace of antiquotation")
     4.9        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    4.10    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    4.11  

     5.1 --- a/src/Pure/General/scan.ML	Sat Jul 23 16:12:12 2011 +0200
     5.2 +++ b/src/Pure/General/scan.ML	Sat Jul 23 16:37:17 2011 +0200
     5.3 @@ -11,8 +11,9 @@
     5.4  
     5.5  signature BASIC_SCAN =
     5.6  sig
     5.7 +  type message = unit -> string
     5.8    (*error msg handler*)
     5.9 -  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
    5.10 +  val !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b
    5.11    (*apply function*)
    5.12    val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    5.13    (*alternative*)
    5.14 @@ -41,7 +42,7 @@
    5.15    val error: ('a -> 'b) -> 'a -> 'b
    5.16    val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
    5.17    val fail: 'a -> 'b
    5.18 -  val fail_with: ('a -> string) -> 'a -> 'b
    5.19 +  val fail_with: ('a -> message) -> 'a -> 'b
    5.20    val succeed: 'a -> 'b -> 'a * 'b
    5.21    val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
    5.22    val one: ('a -> bool) -> 'a list -> 'a * 'a list
    5.23 @@ -93,19 +94,21 @@
    5.24  
    5.25  (* exceptions *)
    5.26  
    5.27 +type message = unit -> string;
    5.28 +
    5.29  exception MORE of string option;        (*need more input (prompt)*)
    5.30 -exception FAIL of string option;        (*try alternatives (reason of failure)*)
    5.31 -exception ABORT of string;              (*dead end*)
    5.32 +exception FAIL of message option;       (*try alternatives (reason of failure)*)
    5.33 +exception ABORT of message;             (*dead end*)
    5.34  
    5.35  fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    5.36  fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    5.37  fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    5.38  fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    5.39 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
    5.40 +fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
    5.41  
    5.42  fun catch scan xs = scan xs
    5.43 -  handle ABORT msg => raise Fail msg
    5.44 -    | FAIL msg => raise Fail (the_default "Syntax error" msg);
    5.45 +  handle ABORT msg => raise Fail (msg ())
    5.46 +    | FAIL msg => raise Fail (case msg of NONE => "Syntax error" | SOME m => m ());
    5.47  
    5.48  
    5.49  (* scanner combinators *)
    5.50 @@ -236,7 +239,7 @@
    5.51  
    5.52  fun finite' (Stopper (mk_stopper, is_stopper)) scan (state, input) =
    5.53    let
    5.54 -    fun lost () = raise ABORT "Bad scanner: lost stopper of finite scan!";
    5.55 +    fun lost () = raise ABORT (fn () => "Bad scanner: lost stopper of finite scan!");
    5.56  
    5.57      fun stop [] = lost ()
    5.58        | stop lst =
    5.59 @@ -244,7 +247,7 @@
    5.60            in if is_stopper x then ((), xs) else lost () end;
    5.61    in
    5.62      if exists is_stopper input then
    5.63 -      raise ABORT "Stopper may not occur in input of finite scan!"
    5.64 +      raise ABORT (fn () => "Stopper may not occur in input of finite scan!")
    5.65      else (strict scan --| lift stop) (state, input @ [mk_stopper input])
    5.66    end;
    5.67  

     6.1 --- a/src/Pure/General/symbol.ML	Sat Jul 23 16:12:12 2011 +0200
     6.2 +++ b/src/Pure/General/symbol.ML	Sat Jul 23 16:37:17 2011 +0200
     6.3 @@ -404,13 +404,13 @@
     6.4  
     6.5  fun scanner msg scan chs =
     6.6    let
     6.7 -    fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs)
     6.8 -      | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
     6.9 +    fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))
    6.10 +      | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));
    6.11      val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
    6.12    in
    6.13      (case fin_scan chs of
    6.14        (result, []) => result
    6.15 -    | (_, rest) => error (message (rest, NONE)))
    6.16 +    | (_, rest) => error (message (rest, NONE) ()))
    6.17    end;
    6.18  
    6.19  val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);

     7.1 --- a/src/Pure/General/symbol_pos.ML	Sat Jul 23 16:12:12 2011 +0200
     7.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Jul 23 16:37:17 2011 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4    val content: T list -> string
     7.5    val is_eof: T -> bool
     7.6    val stopper: T Scan.stopper
     7.7 -  val !!! : string -> (T list -> 'a) -> T list -> 'a
     7.8 +  val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
     7.9    val change_prompt: ('a -> 'b) -> 'a -> 'b
    7.10    val scan_pos: T list -> Position.T * T list
    7.11    val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    7.12 @@ -65,9 +65,9 @@
    7.13      fun get_pos [] = " (past end-of-text!)"
    7.14        | get_pos ((_, pos) :: _) = Position.str_of pos;
    7.15  
    7.16 -    fun err (syms, msg) =
    7.17 -      text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
    7.18 -      (case msg of NONE => "" | SOME s => "\n" ^ s);
    7.19 +    fun err (syms, msg) = fn () =>
    7.20 +      text () ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
    7.21 +      (case msg of NONE => "" | SOME m => "\n" ^ m ());
    7.22    in Scan.!! err scan end;
    7.23  
    7.24  fun change_prompt scan = Scan.prompt "# " scan;
    7.25 @@ -91,11 +91,11 @@
    7.26      in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    7.27  
    7.28  fun scan_str q =
    7.29 -  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
    7.30 +  $$$ "\\" |-- !!! (fn () => "bad escape character in string") ($$$ q || $$$ "\\" || char_code) ||
    7.31    Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    7.32  
    7.33  fun scan_strs q =
    7.34 -  (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
    7.35 +  (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
    7.36      (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    7.37  
    7.38  in

     8.1 --- a/src/Pure/General/xml.ML	Sat Jul 23 16:12:12 2011 +0200
     8.2 +++ b/src/Pure/General/xml.ML	Sat Jul 23 16:37:17 2011 +0200
     8.3 @@ -138,8 +138,8 @@
     8.4  
     8.5  local
     8.6  
     8.7 -fun err s (xs, _) =
     8.8 -  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
     8.9 +fun err msg (xs, _) =
    8.10 +  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
    8.11  
    8.12  fun ignored _ = [];
    8.13  
    8.14 @@ -202,10 +202,10 @@
    8.15  and parse_element xs =
    8.16    ($$ "<" |-- Symbol.scan_id --
    8.17      Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) =>
    8.18 -      !! (err "Expected > or />")
    8.19 +      !! (err (fn () => "Expected > or />"))
    8.20          (Scan.this_string "/>" >> ignored
    8.21           || $$ ">" |-- parse_content --|
    8.22 -            !! (err ("Expected </" ^ s ^ ">"))
    8.23 +            !! (err (fn () => "Expected </" ^ s ^ ">"))
    8.24                (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
    8.25  
    8.26  val parse_document =
    8.27 @@ -213,7 +213,7 @@
    8.28    |-- parse_element;
    8.29  
    8.30  fun parse s =
    8.31 -  (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
    8.32 +  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
    8.33        (blanks |-- parse_document --| blanks))) (raw_explode s) of
    8.34      (x, []) => x
    8.35    | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));

     9.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:12:12 2011 +0200
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:37:17 2011 +0200
     9.3 @@ -775,8 +775,8 @@
     9.4      (props_text :|-- (fn (pos, str) =>
     9.5        (case Outer_Syntax.parse pos str of
     9.6          [tr] => Scan.succeed (K tr)
     9.7 -      | _ => Scan.fail_with (K "exactly one command expected"))
     9.8 -      handle ERROR msg => Scan.fail_with (K msg)));
     9.9 +      | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
    9.10 +      handle ERROR msg => Scan.fail_with (K (fn () => msg))));
    9.11  
    9.12  
    9.13  

    10.1 --- a/src/Pure/Isar/parse.ML	Sat Jul 23 16:12:12 2011 +0200
    10.2 +++ b/src/Pure/Isar/parse.ML	Sat Jul 23 16:37:17 2011 +0200
    10.3 @@ -115,13 +115,14 @@
    10.4  (* group atomic parsers (no cuts!) *)
    10.5  
    10.6  fun fail_with s = Scan.fail_with
    10.7 -  (fn [] => s ^ " expected (past end-of-file!)"
    10.8 +  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
    10.9      | tok :: _ =>
   10.10 -        (case Token.text_of tok of
   10.11 -          (txt, "") =>
   10.12 -            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
   10.13 -        | (txt1, txt2) =>
   10.14 -            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
   10.15 +        (fn () =>
   10.16 +          (case Token.text_of tok of
   10.17 +            (txt, "") =>
   10.18 +              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
   10.19 +          | (txt1, txt2) =>
   10.20 +              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
   10.21  
   10.22  fun group s scan = scan || fail_with s;
   10.23  
   10.24 @@ -133,10 +134,13 @@
   10.25      fun get_pos [] = " (past end-of-file!)"
   10.26        | get_pos (tok :: _) = Token.pos_of tok;
   10.27  
   10.28 -    fun err (toks, NONE) = kind ^ get_pos toks
   10.29 +    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
   10.30        | err (toks, SOME msg) =
   10.31 -          if String.isPrefix kind msg then msg
   10.32 -          else kind ^ get_pos toks ^ ": " ^ msg;
   10.33 +          (fn () =>
   10.34 +            let val s = msg () in
   10.35 +              if String.isPrefix kind s then s
   10.36 +              else kind ^ get_pos toks ^ ": " ^ s
   10.37 +            end);
   10.38    in Scan.!! err scan end;
   10.39  
   10.40  fun !!! scan = cut "Outer syntax error" scan;

    11.1 --- a/src/Pure/Isar/token.ML	Sat Jul 23 16:12:12 2011 +0200
    11.2 +++ b/src/Pure/Isar/token.ML	Sat Jul 23 16:37:17 2011 +0200
    11.3 @@ -50,7 +50,6 @@
    11.4    val assign: value option -> T -> unit
    11.5    val closure: T -> T
    11.6    val ident_or_symbolic: string -> bool
    11.7 -  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
    11.8    val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
    11.9    val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
   11.10      (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
   11.11 @@ -257,7 +256,7 @@
   11.12  
   11.13  open Basic_Symbol_Pos;
   11.14  
   11.15 -fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
   11.16 +fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
   11.17  
   11.18  
   11.19  (* scan symbolic idents *)

    12.1 --- a/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:12:12 2011 +0200
    12.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:37:17 2011 +0200
    12.3 @@ -136,7 +136,7 @@
    12.4  
    12.5  open Basic_Symbol_Pos;
    12.6  
    12.7 -fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
    12.8 +fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
    12.9  
   12.10  
   12.11  (* blanks *)

    13.1 --- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:12:12 2011 +0200
    13.2 +++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
    13.3 @@ -20,13 +20,13 @@
    13.4      fun get_pos [] = " (past end-of-file!)"
    13.5        | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
    13.6  
    13.7 -    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
    13.8 -      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
    13.9 +    fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
   13.10 +      | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
   13.11    in Scan.!! err scan end;
   13.12  
   13.13  fun bad_input x =
   13.14    (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
   13.15 -    (fn msg => Scan.fail_with (K msg))) x;
   13.16 +    (fn msg => Scan.fail_with (K (fn () => msg)))) x;
   13.17  
   13.18  
   13.19  (** basic parsers **)

    14.1 --- a/src/Pure/Syntax/lexicon.ML	Sat Jul 23 16:12:12 2011 +0200
    14.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Jul 23 16:37:17 2011 +0200
    14.3 @@ -114,7 +114,7 @@
    14.4  
    14.5  open Basic_Symbol_Pos;
    14.6  
    14.7 -fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
    14.8 +fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
    14.9  
   14.10  val scan_id =
   14.11    Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::

    15.1 --- a/src/Pure/Thy/rail.ML	Sat Jul 23 16:12:12 2011 +0200
    15.2 +++ b/src/Pure/Thy/rail.ML	Sat Jul 23 16:37:17 2011 +0200
    15.3 @@ -72,7 +72,7 @@
    15.4  
    15.5  val scan =
    15.6    (Scan.repeat scan_token >> flat) --|
    15.7 -    Symbol_Pos.!!! "Rail lexical error: bad input"
    15.8 +    Symbol_Pos.!!! (fn () => "Rail lexical error: bad input")
    15.9        (Scan.ahead (Scan.one Symbol_Pos.is_eof));
   15.10  
   15.11  in
   15.12 @@ -92,17 +92,20 @@
   15.13      fun get_pos [] = " (past end-of-file!)"
   15.14        | get_pos (tok :: _) = Position.str_of (pos_of tok);
   15.15  
   15.16 -    fun err (toks, NONE) = prefix ^ get_pos toks
   15.17 +    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
   15.18        | err (toks, SOME msg) =
   15.19 -          if String.isPrefix prefix msg then msg
   15.20 -          else prefix ^ get_pos toks ^ ": " ^ msg;
   15.21 +          (fn () =>
   15.22 +            let val s = msg () in
   15.23 +              if String.isPrefix prefix s then s
   15.24 +              else prefix ^ get_pos toks ^ ": " ^ s
   15.25 +            end);
   15.26    in Scan.!! err scan end;
   15.27  
   15.28  fun $$$ x =
   15.29    Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   15.30    Scan.fail_with
   15.31 -    (fn [] => print_keyword x ^ " expected (past end-of-file!)"
   15.32 -      | tok :: _ => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found");
   15.33 +    (fn [] => (fn () => print_keyword x ^ " expected (past end-of-file!)")
   15.34 +      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
   15.35  
   15.36  fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   15.37  fun enum sep scan = enum1 sep scan || Scan.succeed [];

    16.1 --- a/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:12:12 2011 +0200
    16.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:37:17 2011 +0200
    16.3 @@ -355,7 +355,7 @@
    16.4    Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
    16.5      >> pair (d + 1)) ||
    16.6    Scan.depend (fn d => Scan.one Token.is_end_ignore --|
    16.7 -    (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
    16.8 +    (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
    16.9      >> pair (d - 1));
   16.10  
   16.11  val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);

    17.1 --- a/src/Tools/Code/code_printer.ML	Sat Jul 23 16:12:12 2011 +0200
    17.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jul 23 16:37:17 2011 +0200
    17.3 @@ -101,7 +101,8 @@
    17.4  
    17.5  (** generic nonsense *)
    17.6  
    17.7 -fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
    17.8 +fun eqn_error (SOME thm) s =
    17.9 +      error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
   17.10    | eqn_error NONE s = error s;
   17.11  
   17.12  val code_presentationN = "code_presentation";
   17.13 @@ -132,10 +133,10 @@
   17.14  
   17.15  fun filter_presentation [] tree =
   17.16        Buffer.empty
   17.17 -      |> fold XML.add_content tree 
   17.18 +      |> fold XML.add_content tree
   17.19    | filter_presentation presentation_names tree =
   17.20        let
   17.21 -        fun is_selected (name, attrs) = 
   17.22 +        fun is_selected (name, attrs) =
   17.23            name = code_presentationN
   17.24            andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
   17.25          fun add_content_with_space tree (is_first, buf) =
   17.26 @@ -169,8 +170,9 @@
   17.27      val namemap' = fold2 (curry Symtab.update) names names' namemap;
   17.28    in (namemap', namectxt') end;
   17.29  
   17.30 -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
   17.31 - of SOME name' => name'
   17.32 +fun lookup_var (namemap, _) name =
   17.33 +  case Symtab.lookup namemap name of
   17.34 +    SOME name' => name'
   17.35    | NONE => error ("Invalid name in context: " ^ quote name);
   17.36  
   17.37  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
   17.38 @@ -190,7 +192,7 @@
   17.39      val vars' = intro_vars fished3 vars;
   17.40    in map (lookup_var vars') fished3 end;
   17.41  
   17.42 -fun intro_base_names no_syntax deresolve names = names 
   17.43 +fun intro_base_names no_syntax deresolve names = names
   17.44    |> map_filter (fn name => if no_syntax name then
   17.45        let val name' = deresolve name in
   17.46          if Long_Name.is_qualified name' then NONE else SOME name'
   17.47 @@ -297,7 +299,8 @@
   17.48    | requires_args (complex_const_syntax (k, _)) = k;
   17.49  
   17.50  fun simple_const_syntax syn =
   17.51 -  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
   17.52 +  complex_const_syntax
   17.53 +    (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
   17.54  
   17.55  type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   17.56    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
   17.57 @@ -311,20 +314,24 @@
   17.58        fold_map (Code_Thingol.ensure_declared_const thy) cs naming
   17.59        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
   17.60  
   17.61 -fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
   17.62 -  case const_syntax c
   17.63 -   of NONE => brackify fxy (print_app_expr some_thm vars app)
   17.64 -    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
   17.65 -    | SOME (Complex_const_syntax (k, print)) =>
   17.66 -        let
   17.67 -          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
   17.68 -        in if k = length ts
   17.69 -          then print' fxy ts
   17.70 +fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
   17.71 +    (app as ((c, (_, function_typs)), ts)) =
   17.72 +  case const_syntax c of
   17.73 +    NONE => brackify fxy (print_app_expr some_thm vars app)
   17.74 +  | SOME (Plain_const_syntax (_, s)) =>
   17.75 +      brackify fxy (str s :: map (print_term some_thm vars BR) ts)
   17.76 +  | SOME (Complex_const_syntax (k, print)) =>
   17.77 +      let
   17.78 +        fun print' fxy ts =
   17.79 +          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
   17.80 +      in
   17.81 +        if k = length ts
   17.82 +        then print' fxy ts
   17.83          else if k < length ts
   17.84 -          then case chop k ts of (ts1, ts2) =>
   17.85 -            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
   17.86 -          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
   17.87 -        end;
   17.88 +        then case chop k ts of (ts1, ts2) =>
   17.89 +          brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
   17.90 +        else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
   17.91 +      end;
   17.92  
   17.93  fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   17.94    let
   17.95 @@ -377,12 +384,14 @@
   17.96             (   $$ "'" |-- sym_any
   17.97              || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   17.98                   sym_any) >> (String o implode)));
   17.99 -  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
  17.100 -   of ((false, [String s]), []) => mk_plain s
  17.101 +    fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
  17.102 +      | err _ (_, SOME msg) = msg;
  17.103 +  in
  17.104 +    case Scan.finite Symbol.stopper parse (Symbol.explode s) of
  17.105 +      ((false, [String s]), []) => mk_plain s
  17.106      | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
  17.107      | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
  17.108 -    | _ => Scan.!!
  17.109 -        (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
  17.110 +    | _ => Scan.!! (err s) Scan.fail ()
  17.111    end;
  17.112  
  17.113  val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");

    18.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:12:12 2011 +0200
    18.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:37:17 2011 +0200
    18.3 @@ -103,12 +103,13 @@
    18.4        Scan.literal keywords >> token Keyword ||
    18.5        scan_ascii_symbol ||
    18.6        Lexicon.scan_id >> token Name;
    18.7 -    val scan_token = Symbol_Pos.!!! "Lexical error" (Scan.bulk scanner);
    18.8 +    val scan_token = Symbol_Pos.!!! (fn () => "Lexical error") (Scan.bulk scanner);
    18.9    in
   18.10      (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
   18.11        (toks, []) => toks
   18.12 -    | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss
   18.13 -                        ^ Position.str_of (#1 (Symbol_Pos.range ss))))
   18.14 +    | (_, ss) =>
   18.15 +        error ("Lexical error at: " ^ Symbol_Pos.content ss ^
   18.16 +          Position.str_of (#1 (Symbol_Pos.range ss))))
   18.17    end;
   18.18  
   18.19  val stopper =