src/Pure/Thy/rail.ML
changeset 43947 9b00f09f7721
parent 43564 9864182c6bad
child 48764 4fe0920d5049
     1.1 --- a/src/Pure/Thy/rail.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/Thy/rail.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5  val scan =
     1.6    (Scan.repeat scan_token >> flat) --|
     1.7 -    Symbol_Pos.!!! "Rail lexical error: bad input"
     1.8 +    Symbol_Pos.!!! (fn () => "Rail lexical error: bad input")
     1.9        (Scan.ahead (Scan.one Symbol_Pos.is_eof));
    1.10  
    1.11  in
    1.12 @@ -92,17 +92,20 @@
    1.13      fun get_pos [] = " (past end-of-file!)"
    1.14        | get_pos (tok :: _) = Position.str_of (pos_of tok);
    1.15  
    1.16 -    fun err (toks, NONE) = prefix ^ get_pos toks
    1.17 +    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
    1.18        | err (toks, SOME msg) =
    1.19 -          if String.isPrefix prefix msg then msg
    1.20 -          else prefix ^ get_pos toks ^ ": " ^ msg;
    1.21 +          (fn () =>
    1.22 +            let val s = msg () in
    1.23 +              if String.isPrefix prefix s then s
    1.24 +              else prefix ^ get_pos toks ^ ": " ^ s
    1.25 +            end);
    1.26    in Scan.!! err scan end;
    1.27  
    1.28  fun $$$ x =
    1.29    Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
    1.30    Scan.fail_with
    1.31 -    (fn [] => print_keyword x ^ " expected (past end-of-file!)"
    1.32 -      | tok :: _ => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found");
    1.33 +    (fn [] => (fn () => print_keyword x ^ " expected (past end-of-file!)")
    1.34 +      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
    1.35  
    1.36  fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
    1.37  fun enum sep scan = enum1 sep scan || Scan.succeed [];