# HG changeset patch # User wenzelm # Date 1344544264 -7200 # Node ID c197b3c3e7fa7326c262d221d53b1ba84bdfa956 # Parent 89b4e7d83d6f8c92afd0e2d42db758467bbf37a4 some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view; diff -r 89b4e7d83d6f -r c197b3c3e7fa src/Pure/Isar/outer_syntax.ML --- 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} = diff -r 89b4e7d83d6f -r c197b3c3e7fa src/Pure/Isar/token.ML --- 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 *) diff -r 89b4e7d83d6f -r c197b3c3e7fa src/Pure/Thy/thy_syntax.ML --- 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;