tuned messages: end-of-input rarely means physical end-of-file from the past;
authorwenzelm
Thu Aug 23 17:46:03 2012 +0200 (2012-08-23)
changeset 489115debc3e4fa81
parent 48910 1c8c15c30356
child 48912 ffdb37019b2f
tuned messages: end-of-input rarely means physical end-of-file from the past;
src/HOL/SPARK/Tools/fdl_lexer.ML
src/HOL/SPARK/Tools/fdl_parser.ML
src/Pure/General/file.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse.scala
src/Pure/Isar/token.ML
src/Pure/ML/ml_parse.ML
src/Pure/Thy/rail.ML
     1.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Aug 23 15:44:47 2012 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Aug 23 17:46:03 2012 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5  fun !!! text scan =
     1.6    let
     1.7 -    fun get_pos [] = " (past end-of-text!)"
     1.8 +    fun get_pos [] = " (end-of-input)"
     1.9        | get_pos ((_, pos) :: _) = Position.str_of pos;
    1.10  
    1.11      fun err (syms, msg) = fn () =>
     2.1 --- a/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Aug 23 15:44:47 2012 +0200
     2.2 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Aug 23 17:46:03 2012 +0200
     2.3 @@ -69,7 +69,7 @@
     2.4  
     2.5  fun !!! scan =
     2.6    let
     2.7 -    fun get_pos [] = " (past end-of-file!)"
     2.8 +    fun get_pos [] = " (end-of-input)"
     2.9        | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
    2.10  
    2.11      fun err (syms, msg) = fn () =>
     3.1 --- a/src/Pure/General/file.ML	Thu Aug 23 15:44:47 2012 +0200
     3.2 +++ b/src/Pure/General/file.ML	Thu Aug 23 17:46:03 2012 +0200
     3.3 @@ -128,7 +128,7 @@
     3.4  (*
     3.5    scalable iterator:
     3.6    . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
     3.7 -  . optional terminator at end-of-file
     3.8 +  . optional terminator at end-of-input
     3.9  *)
    3.10  fun fold_chunks terminator f path a = open_input (fn file =>
    3.11    let
     4.1 --- a/src/Pure/General/symbol_pos.ML	Thu Aug 23 15:44:47 2012 +0200
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Aug 23 17:46:03 2012 +0200
     4.3 @@ -66,7 +66,7 @@
     4.4  
     4.5  fun !!! text scan =
     4.6    let
     4.7 -    fun get_pos [] = " (past end-of-text!)"
     4.8 +    fun get_pos [] = " (end-of-input)"
     4.9        | get_pos ((_, pos) :: _) = Position.str_of pos;
    4.10  
    4.11      fun err (syms, msg) = fn () =>
     5.1 --- a/src/Pure/Isar/parse.ML	Thu Aug 23 15:44:47 2012 +0200
     5.2 +++ b/src/Pure/Isar/parse.ML	Thu Aug 23 17:46:03 2012 +0200
     5.3 @@ -115,7 +115,7 @@
     5.4  (* group atomic parsers (no cuts!) *)
     5.5  
     5.6  fun group s scan = scan || Scan.fail_with
     5.7 -  (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
     5.8 +  (fn [] => (fn () => s () ^ " expected,\nbut end-of-input was found")
     5.9      | tok :: _ =>
    5.10          (fn () =>
    5.11            (case Token.text_of tok of
    5.12 @@ -129,7 +129,7 @@
    5.13  
    5.14  fun cut kind scan =
    5.15    let
    5.16 -    fun get_pos [] = " (past end-of-file!)"
    5.17 +    fun get_pos [] = " (end-of-input)"
    5.18        | get_pos (tok :: _) = Token.pos_of tok;
    5.19  
    5.20      fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
     6.1 --- a/src/Pure/Isar/parse.scala	Thu Aug 23 15:44:47 2012 +0200
     6.2 +++ b/src/Pure/Isar/parse.scala	Thu Aug 23 17:46:03 2012 +0200
     6.3 @@ -29,7 +29,7 @@
     6.4        def apply(raw_input: Input) =
     6.5        {
     6.6          val in = proper(raw_input)
     6.7 -        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
     6.8 +        if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
     6.9          else {
    6.10            val token = in.first
    6.11            if (pred(token)) Success(token, proper(in.rest))
     7.1 --- a/src/Pure/Isar/token.ML	Thu Aug 23 15:44:47 2012 +0200
     7.2 +++ b/src/Pure/Isar/token.ML	Thu Aug 23 17:46:03 2012 +0200
     7.3 @@ -122,7 +122,7 @@
     7.4    | InternalValue => "internal value"
     7.5    | Error _ => "bad input"
     7.6    | Sync => "sync marker"
     7.7 -  | EOF => "end-of-file";
     7.8 +  | EOF => "end-of-input";
     7.9  
    7.10  
    7.11  (* position *)
     8.1 --- a/src/Pure/ML/ml_parse.ML	Thu Aug 23 15:44:47 2012 +0200
     8.2 +++ b/src/Pure/ML/ml_parse.ML	Thu Aug 23 17:46:03 2012 +0200
     8.3 @@ -17,7 +17,7 @@
     8.4  
     8.5  fun !!! scan =
     8.6    let
     8.7 -    fun get_pos [] = " (past end-of-file!)"
     8.8 +    fun get_pos [] = " (end-of-input)"
     8.9        | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
    8.10  
    8.11      fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
     9.1 --- a/src/Pure/Thy/rail.ML	Thu Aug 23 15:44:47 2012 +0200
     9.2 +++ b/src/Pure/Thy/rail.ML	Thu Aug 23 17:46:03 2012 +0200
     9.3 @@ -31,7 +31,7 @@
     9.4    | Ident => "identifier"
     9.5    | String => "single-quoted string"
     9.6    | Antiq _ => "antiquotation"
     9.7 -  | EOF => "end-of-file";
     9.8 +  | EOF => "end-of-input";
     9.9  
    9.10  fun print (Token ((pos, _), (k, x))) =
    9.11    (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
    9.12 @@ -91,7 +91,7 @@
    9.13    let
    9.14      val prefix = "Rail syntax error";
    9.15  
    9.16 -    fun get_pos [] = " (past end-of-file!)"
    9.17 +    fun get_pos [] = " (end-of-input)"
    9.18        | get_pos (tok :: _) = Position.str_of (pos_of tok);
    9.19  
    9.20      fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
    9.21 @@ -106,7 +106,7 @@
    9.22  fun $$$ x =
    9.23    Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
    9.24    Scan.fail_with
    9.25 -    (fn [] => (fn () => print_keyword x ^ " expected (past end-of-file!)")
    9.26 +    (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
    9.27        | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
    9.28  
    9.29  fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);