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;