src/Pure/Syntax/lexicon.ML

   val varT: typ
   val tidT: typ
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: token -> unit
+  val report_token: Proof.context -> token -> unit
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
   val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list
 end;

   | StrSy       => Markup.xstr
   | Space       => Markup.none
   | Comment     => Markup.inner_comment
   | EOF         => Markup.none;
 
-fun report_token (Token (kind, _, (pos, _))) =
-  Position.report (token_kind_markup kind) pos;
+fun report_token ctxt (Token (kind, _, (pos, _))) =
+  ContextPosition.report ctxt (token_kind_markup kind) pos;
 
 
 (* matching_tokens *)
 
 fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y