src/Pure/Thy/thy_syntax.ML

   | Token.AltString     => Isabelle_Markup.altstring
   | Token.Verbatim      => Isabelle_Markup.verbatim
   | Token.Space         => Markup.empty
   | Token.Comment       => Isabelle_Markup.comment
   | Token.InternalValue => Markup.empty
-  | Token.Error _       => Isabelle_Markup.bad
+  | Token.Error msg     => Isabelle_Markup.bad msg
   | Token.Sync          => Isabelle_Markup.control
   | Token.EOF           => Isabelle_Markup.control;
 
 fun token_markup tok =
   if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Isabelle_Markup.operator

 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.bad) else NONE);
+          if Symbol.is_malformed sym
+          then SOME (pos, Isabelle_Markup.bad "Malformed symbol") 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