src/Pure/Isar/parse.ML
changeset 43947 9b00f09f7721
parent 43775 b361c7d184e7
child 44357 5f5649ac8235
     1.1 --- a/src/Pure/Isar/parse.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/Isar/parse.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -115,13 +115,14 @@
     1.4  (* group atomic parsers (no cuts!) *)
     1.5  
     1.6  fun fail_with s = Scan.fail_with
     1.7 -  (fn [] => s ^ " expected (past end-of-file!)"
     1.8 +  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
     1.9      | tok :: _ =>
    1.10 -        (case Token.text_of tok of
    1.11 -          (txt, "") =>
    1.12 -            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    1.13 -        | (txt1, txt2) =>
    1.14 -            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
    1.15 +        (fn () =>
    1.16 +          (case Token.text_of tok of
    1.17 +            (txt, "") =>
    1.18 +              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    1.19 +          | (txt1, txt2) =>
    1.20 +              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
    1.21  
    1.22  fun group s scan = scan || fail_with s;
    1.23  
    1.24 @@ -133,10 +134,13 @@
    1.25      fun get_pos [] = " (past end-of-file!)"
    1.26        | get_pos (tok :: _) = Token.pos_of tok;
    1.27  
    1.28 -    fun err (toks, NONE) = kind ^ get_pos toks
    1.29 +    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
    1.30        | err (toks, SOME msg) =
    1.31 -          if String.isPrefix kind msg then msg
    1.32 -          else kind ^ get_pos toks ^ ": " ^ msg;
    1.33 +          (fn () =>
    1.34 +            let val s = msg () in
    1.35 +              if String.isPrefix kind s then s
    1.36 +              else kind ^ get_pos toks ^ ": " ^ s
    1.37 +            end);
    1.38    in Scan.!! err scan end;
    1.39  
    1.40  fun !!! scan = cut "Outer syntax error" scan;