tuned errors;
authorwenzelm
Mon Jan 20 16:56:18 2014 +0100 (2014-01-20)
changeset 5510357d87ec3da4c
parent 55053 f69530f22f5a
child 55104 8284c0d5bf52
tuned errors;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:14:19 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:56:18 2014 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    type T = Symbol.symbol * Position.T
     1.6    val symbol: T -> Symbol.symbol
     1.7 +  val $$ : Symbol.symbol -> T list -> T * T list
     1.8    val $$$ : Symbol.symbol -> T list -> T list * T list
     1.9    val ~$$$ : Symbol.symbol -> T list -> T list * T list
    1.10    val content: T list -> string
    1.11 @@ -115,8 +116,10 @@
    1.12    Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    1.13  
    1.14  fun scan_strs q err_prefix =
    1.15 -  (scan_pos --| $$$ q) -- !!! (fn () => err_prefix ^ "missing quote at end of string")
    1.16 -    (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
    1.17 +  Scan.ahead ($$ q) |--
    1.18 +    !!! (fn () => err_prefix ^ "unclosed string literal")
    1.19 +      ((scan_pos --| $$$ q) --
    1.20 +        (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))));
    1.21  
    1.22  fun recover_strs q =
    1.23    $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
    1.24 @@ -284,6 +287,7 @@
    1.25  
    1.26  structure Basic_Symbol_Pos =   (*not open by default*)
    1.27  struct
    1.28 +  val $$ = Symbol_Pos.$$;
    1.29    val $$$ = Symbol_Pos.$$$;
    1.30    val ~$$$ = Symbol_Pos.~$$$;
    1.31  end;
     2.1 --- a/src/Pure/Isar/token.ML	Mon Jan 20 16:14:19 2014 +0100
     2.2 +++ b/src/Pure/Isar/token.ML	Mon Jan 20 16:56:18 2014 +0100
     2.3 @@ -116,10 +116,10 @@
     2.4    | TypeVar => "schematic type variable"
     2.5    | Nat => "natural number"
     2.6    | Float => "floating-point number"
     2.7 -  | String => "string"
     2.8 +  | String => "quoted string"
     2.9    | AltString => "back-quoted string"
    2.10    | Verbatim => "verbatim text"
    2.11 -  | Cartouche => "cartouche"
    2.12 +  | Cartouche => "text cartouche"
    2.13    | Space => "white space"
    2.14    | Comment => "comment text"
    2.15    | InternalValue => "internal value"
     3.1 --- a/src/Pure/ML/ml_lex.ML	Mon Jan 20 16:14:19 2014 +0100
     3.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Jan 20 16:56:18 2014 +0100
     3.3 @@ -241,8 +241,9 @@
     3.4    $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) [];
     3.5  
     3.6  val scan_string =
     3.7 -  $$$ "\"" @@@ !!! "missing quote at end of string"
     3.8 -    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
     3.9 +  Scan.ahead ($$ "\"") |--
    3.10 +    !!! "unclosed string literal"
    3.11 +      ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
    3.12  
    3.13  val recover_string =
    3.14    $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
    3.15 @@ -304,9 +305,7 @@
    3.16            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    3.17          |> Source.exhaust
    3.18          |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
    3.19 -        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
    3.20 -      handle ERROR msg =>
    3.21 -        cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
    3.22 +        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
    3.23    in input @ termination end;
    3.24  
    3.25  end;