tuned messages: end-of-input rarely means physical end-of-file from the past;

--- 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 () =>

--- 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 () =>

--- 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

--- 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 () =>

--- 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)

--- 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))

--- 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 *)

--- 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)

--- 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);