src/Pure/Thy/thy_syntax.ML

       Symbol_Pos.explode (text, pos)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val (markup, msg) = Token.markup tok;
-    val reports = ((Token.pos_of tok, markup), msg) :: malformed_symbols;
+    val reports = Token.report tok :: Token.completion_report 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 (fst (Token.markup tok)) (Output.output (Token.unparse tok));
+  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
 
 end;