# HG changeset patch # User wenzelm # Date 1345736763 -7200 # Node ID 5debc3e4fa81f1e6e4485774dc028beb0d79e858 # Parent 1c8c15c30356525e840baf8689b23b3a60b49465 tuned messages: end-of-input rarely means physical end-of-file from the past; diff -r 1c8c15c30356 -r 5debc3e4fa81 src/HOL/SPARK/Tools/fdl_lexer.ML --- a/src/HOL/SPARK/Tools/fdl_lexer.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Thu Aug 23 17:46:03 2012 +0200 @@ -191,7 +191,7 @@ fun !!! text scan = let - fun get_pos [] = " (past end-of-text!)" + fun get_pos [] = " (end-of-input)" | get_pos ((_, pos) :: _) = Position.str_of pos; fun err (syms, msg) = fn () => diff -r 1c8c15c30356 -r 5debc3e4fa81 src/HOL/SPARK/Tools/fdl_parser.ML --- a/src/HOL/SPARK/Tools/fdl_parser.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML Thu Aug 23 17:46:03 2012 +0200 @@ -69,7 +69,7 @@ fun !!! scan = let - fun get_pos [] = " (past end-of-file!)" + fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Fdl_Lexer.pos_of tok; fun err (syms, msg) = fn () => diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/General/file.ML Thu Aug 23 17:46:03 2012 +0200 @@ -128,7 +128,7 @@ (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine - . optional terminator at end-of-file + . optional terminator at end-of-input *) fun fold_chunks terminator f path a = open_input (fn file => let diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/General/symbol_pos.ML Thu Aug 23 17:46:03 2012 +0200 @@ -66,7 +66,7 @@ fun !!! text scan = let - fun get_pos [] = " (past end-of-text!)" + fun get_pos [] = " (end-of-input)" | get_pos ((_, pos) :: _) = Position.str_of pos; fun err (syms, msg) = fn () => diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/Isar/parse.ML Thu Aug 23 17:46:03 2012 +0200 @@ -115,7 +115,7 @@ (* group atomic parsers (no cuts!) *) fun group s scan = scan || Scan.fail_with - (fn [] => (fn () => s () ^ " expected (past end-of-file!)") + (fn [] => (fn () => s () ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => (case Token.text_of tok of @@ -129,7 +129,7 @@ fun cut kind scan = let - fun get_pos [] = " (past end-of-file!)" + fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Token.pos_of tok; fun err (toks, NONE) = (fn () => kind ^ get_pos toks) diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/Isar/parse.scala Thu Aug 23 17:46:03 2012 +0200 @@ -29,7 +29,7 @@ def apply(raw_input: Input) = { val in = proper(raw_input) - if (in.atEnd) Failure(s + " expected (past end-of-file!)", in) + if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) else { val token = in.first if (pred(token)) Success(token, proper(in.rest)) diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/Isar/token.ML Thu Aug 23 17:46:03 2012 +0200 @@ -122,7 +122,7 @@ | InternalValue => "internal value" | Error _ => "bad input" | Sync => "sync marker" - | EOF => "end-of-file"; + | EOF => "end-of-input"; (* position *) diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/ML/ml_parse.ML --- a/src/Pure/ML/ml_parse.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/ML/ml_parse.ML Thu Aug 23 17:46:03 2012 +0200 @@ -17,7 +17,7 @@ fun !!! scan = let - fun get_pos [] = " (past end-of-file!)" + fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok); fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks) diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/Thy/rail.ML --- a/src/Pure/Thy/rail.ML Thu Aug 23 15:44:47 2012 +0200 +++ b/src/Pure/Thy/rail.ML Thu Aug 23 17:46:03 2012 +0200 @@ -31,7 +31,7 @@ | Ident => "identifier" | String => "single-quoted string" | Antiq _ => "antiquotation" - | EOF => "end-of-file"; + | EOF => "end-of-input"; fun print (Token ((pos, _), (k, x))) = (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^ @@ -91,7 +91,7 @@ let val prefix = "Rail syntax error"; - fun get_pos [] = " (past end-of-file!)" + fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.str_of (pos_of tok); fun err (toks, NONE) = (fn () => prefix ^ get_pos toks) @@ -106,7 +106,7 @@ fun $$$ x = Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) || Scan.fail_with - (fn [] => (fn () => print_keyword x ^ " expected (past end-of-file!)") + (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found")); fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);