tuned error messages, more accurate position;
authorwenzelm
Mon Jan 20 20:24:44 2014 +0100 (2014-01-20)
changeset 55106080c0006e917
parent 55105 75815b3b38a1
child 55107 1a29ea173bf9
tuned error messages, more accurate position;
src/HOL/SPARK/Tools/fdl_lexer.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Jan 20 20:04:52 2014 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Jan 20 20:24:44 2014 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  val any_line = whitespace' |-- any_line' --|
     1.5    newline >> (implode o map symbol);
     1.6  
     1.7 -fun gen_comment a b = $$$ a |-- !!! "missing end of comment"
     1.8 +fun gen_comment a b = $$$ a |-- !!! "unclosed comment"
     1.9    (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment;
    1.10  
    1.11  val c_comment = gen_comment "/*" "*/";
     2.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:04:52 2014 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
     2.3 @@ -204,12 +204,14 @@
     2.4  in
     2.5  
     2.6  fun scan_comment err_prefix =
     2.7 -  $$$ "(" @@@ $$$ "*" @@@
     2.8 -    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
     2.9 +  Scan.ahead ($$ "(" -- $$ "*") |--
    2.10 +    !!! (fn () => err_prefix ^ "unclosed comment")
    2.11 +      ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
    2.12  
    2.13  fun scan_comment_body err_prefix =
    2.14 -  $$$ "(" |-- $$$ "*" |--
    2.15 -    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
    2.16 +  Scan.ahead ($$ "(" -- $$ "*") |--
    2.17 +    !!! (fn () => err_prefix ^ "unclosed comment")
    2.18 +      ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
    2.19  
    2.20  val recover_comment =
    2.21    $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
     3.1 --- a/src/Pure/Isar/token.ML	Mon Jan 20 20:04:52 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:24:44 2014 +0100
     3.3 @@ -325,9 +325,11 @@
     3.4    Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
     3.5  
     3.6  val scan_verbatim =
     3.7 -  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
     3.8 -    (Symbol_Pos.change_prompt
     3.9 -      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
    3.10 +  Scan.ahead ($$$ "{" -- $$$ "*") |--
    3.11 +    !!! "unclosed verbatim text"
    3.12 +      ((Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") --
    3.13 +        Symbol_Pos.change_prompt
    3.14 +          ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
    3.15  
    3.16  val recover_verbatim =
    3.17    $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:04:52 2014 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:24:44 2014 +0100
     4.3 @@ -217,12 +217,14 @@
     4.4    $$$ "'" --| Scan.ahead (~$$$ "'");
     4.5  
     4.6  val scan_str =
     4.7 -  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
     4.8 -    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
     4.9 +  Scan.ahead ($$ "'" -- $$ "'") |--
    4.10 +    !!! "unclosed string literal"
    4.11 +      ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
    4.12  
    4.13  val scan_str_body =
    4.14 -  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
    4.15 -    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
    4.16 +  Scan.ahead ($$$ "'" |-- $$$ "'") |--
    4.17 +    !!! "unclosed string literal"
    4.18 +      ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
    4.19  
    4.20  
    4.21  fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));