some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
--- a/src/Pure/Isar/outer_syntax.ML Thu Aug 09 21:09:24 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Aug 09 22:31:04 2012 +0200
@@ -269,31 +269,38 @@
(* read toplevel commands -- fail-safe *)
-val not_singleton = "Exactly one command expected";
-
fun read_span outer_syntax toks =
let
val commands = lookup_commands outer_syntax;
+
val range_pos = Position.set_range (Token.range toks);
+ val pos =
+ (case find_first Token.is_command toks of
+ SOME tok => Token.position_of tok
+ | NONE => range_pos);
fun command_reports tok =
- if Token.kind_of tok = Token.Command then
+ if Token.is_command tok then
let val name = Token.content_of tok in
(case commands name of
NONE => []
| SOME cmd => [(Token.position_of tok, command_markup false (name, cmd))])
end
else [];
- val _ = Position.reports (maps Thy_Syntax.reports_of_token toks @ maps command_reports toks);
+
+ val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
+ val _ = Position.reports (token_reports @ maps command_reports toks);
in
- (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
- [tr] =>
- if Keyword.is_control (Toplevel.name_of tr) then
- (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
- else (tr, true)
- | [] => (Toplevel.ignored range_pos, false)
- | _ => (Toplevel.malformed range_pos not_singleton, true))
- handle ERROR msg => (Toplevel.malformed range_pos msg, true)
+ if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
+ else
+ (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
+ [tr] =>
+ if Keyword.is_control (Toplevel.name_of tr) then
+ (Toplevel.malformed pos "Illegal control command", true)
+ else (tr, true)
+ | [] => (Toplevel.ignored range_pos, false)
+ | _ => (Toplevel.malformed range_pos "Exactly one command expected", true))
+ handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
fun read_element outer_syntax init {head, proof, proper_proof} =
--- a/src/Pure/Isar/token.ML Thu Aug 09 21:09:24 2012 +0200
+++ b/src/Pure/Isar/token.ML Thu Aug 09 22:31:04 2012 +0200
@@ -34,6 +34,7 @@
val is_comment: T -> bool
val is_begin_ignore: T -> bool
val is_end_ignore: T -> bool
+ val is_error: T -> bool
val is_blank: T -> bool
val is_newline: T -> bool
val source_of: T -> string
@@ -178,6 +179,9 @@
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
| is_end_ignore _ = false;
+fun is_error (Token (_, (Error _, _), _)) = true
+ | is_error _ = false;
+
(* blanks and newlines -- space tokens obey lines *)
--- a/src/Pure/Thy/thy_syntax.ML Thu Aug 09 21:09:24 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Thu Aug 09 22:31:04 2012 +0200
@@ -7,8 +7,8 @@
signature THY_SYNTAX =
sig
val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+ val reports_of_tokens: Token.T list -> bool * Position.report list
val present_token: Token.T -> Output.output
- val reports_of_token: Token.T -> Position.report list
datatype span_kind = Command of string | Ignored | Malformed
type span
val span_kind: span -> span_kind
@@ -69,18 +69,25 @@
else I;
in props (token_kind_markup kind) end;
-fun reports_of_symbol (sym, pos) =
- if Symbol.is_malformed sym then [(pos, Isabelle_Markup.malformed)] else [];
+fun reports_of_token tok =
+ let
+ val malformed_symbols =
+ Symbol_Pos.explode (Token.source_position_of tok)
+ |> map_filter (fn (sym, pos) =>
+ if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.malformed) else NONE);
+ val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
+ val reports = (Token.position_of tok, token_markup tok) :: malformed_symbols;
+ in (is_malformed, reports) end;
in
+fun reports_of_tokens toks =
+ let val results = map reports_of_token toks
+ in (exists fst results, maps snd results) end;
+
fun present_token tok =
Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
-fun reports_of_token tok =
- (Token.position_of tok, token_markup tok) ::
- maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
-
end;