diff --git a/src/Pure/General/symbol.ML b/src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML
+++ b/src/Pure/General/symbol.ML
@@ -1,517 +1,519 @@
 (*  Title:      Pure/General/symbol.ML
     Author:     Makarius
 
 Isabelle text symbols.
 *)
 
 signature SYMBOL =
 sig
   type symbol = string
   val explode: string -> symbol list
   val spaces: int -> string
   val STX: symbol
   val DEL: symbol
   val open_: symbol
   val close: symbol
   val space: symbol
   val is_space: symbol -> bool
   val comment: symbol
   val cancel: symbol
   val latex: symbol
   val marker: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
   val is_symbolic_char: symbol -> bool
   val is_printable: symbol -> bool
   val control_prefix: string
   val control_suffix: string
   val is_control: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
   val stopper: symbol Scan.stopper
   val is_malformed: symbol -> bool
   val malformed_msg: symbol -> string
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
   val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
   val is_ascii_line_terminator: symbol -> bool
   val is_ascii_control: symbol -> bool
   val is_ascii_letdig: symbol -> bool
   val is_ascii_lower: symbol -> bool
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol
   val to_ascii_upper: symbol -> symbol
   val is_ascii_identifier: string -> bool
   val scan_ascii_id: string list -> string * string list
   datatype sym =
     Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
   val decode: symbol -> sym
   val encode: sym -> symbol
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
   val is_letter: symbol -> bool
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
   val is_block_ctrl: symbol -> bool
+  val has_block_ctrl: symbol list -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val beginning: int -> symbol list -> string
   val esc: symbol -> string
   val escape: string -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val split_words: symbol list -> string list
   val explode_words: string -> string list
   val trim_blanks: string -> string
   val bump_init: string -> string
   val bump_string: string -> string
   val sub: symbol
   val sup: symbol
   val bold: symbol
   val make_sub: string -> string
   val make_sup: string -> string
   val make_bold: string -> string
   val length: symbol list -> int
   val output: string -> Output.output * int
 end;
 
 structure Symbol: SYMBOL =
 struct
 
 (** type symbol **)
 
 (*Symbols, which are considered the smallest entities of any Isabelle
   string, may be of the following form:
 
     (1) ASCII: a
     (2) UTF-8: ä
     (2) regular symbols: \<ident>
     (3) control symbols: \<^ident>
 
   Output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools.
 *)
 
 type symbol = string;
 
 val STX = chr 2;
 val DEL = chr 127;
 
 val open_ = "\<open>";
 val close = "\<close>";
 
 val space = chr 32;
 fun is_space s = s = space;
 
 local
   val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
 in
   fun spaces n =
     if n < 64 then Vector.sub (small_spaces, n)
     else
       replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
         Vector.sub (small_spaces, n mod 64);
 end;
 
 val comment = "\<comment>";
 val cancel = "\<^cancel>";
 val latex = "\<^latex>";
 val marker = "\<^marker>";
 
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun raw_symbolic s =
   String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
 
 fun is_symbolic s =
   s <> open_ andalso s <> close andalso raw_symbolic s;
 
 val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 fun is_printable s =
   if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
   else is_utf8 s orelse raw_symbolic s;
 
 val control_prefix = "\092<^";
 val control_suffix = ">";
 
 fun is_control s =
   String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
 
 
 (* input source control *)
 
 val eof = "";
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
 val stopper = Scan.stopper (K eof) is_eof;
 
 fun is_malformed s =
   String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
   orelse s = "\092<>" orelse s = "\092<^>";
 
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
 
 (* ASCII symbols *)
 
 fun is_ascii s = is_char s andalso ord s < 128;
 
 fun is_ascii_letter s =
   is_char s andalso
    (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse
     Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
 
 fun is_ascii_digit s =
   is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9";
 
 fun is_ascii_hex s =
   is_char s andalso
    (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse
     Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse
     Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f");
 
 fun is_ascii_quasi "_" = true
   | is_ascii_quasi "'" = true
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     | _ => false;
 
 val is_ascii_line_terminator =
   fn "\r" => true | "\n" => true | _ => false;
 
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
 
 fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
 
 fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
 fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z");
 
 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s;
 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s;
 
 fun is_ascii_identifier s =
   size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
   forall_string is_ascii_letdig s;
 
 val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
 
 
 (* diagnostics *)
 
 fun beginning n cs =
   let
     val drop_blanks = drop_suffix is_ascii_blank;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
     (drop_blanks (take n all_cs)
       |> map (fn c => if is_ascii_blank c then space else c)
       |> implode) ^ dots
   end;
 
 
 (* symbol variants *)
 
 datatype sym =
   Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF;
 
 fun decode s =
   if s = "" then EOF
   else if is_char s then Char s
   else if is_utf8 s then UTF8 s
   else if is_malformed s then Malformed s
   else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
 fun encode (Char s) = s
   | encode (UTF8 s) = s
   | encode (Sym s) = "\092<" ^ s ^ ">"
   | encode (Control s) = "\092<^" ^ s ^ ">"
   | encode (Malformed s) = s
   | encode EOF = "";
 
 
 (* standard symbol kinds *)
 
 local
   val letter_symbols =
     Symtab.make_set [
       "\<A>",
       "\<B>",
       "\<C>",
       "\<D>",
       "\<E>",
       "\<F>",
       "\<G>",
       "\<H>",
       "\<I>",
       "\<J>",
       "\<K>",
       "\<L>",
       "\<M>",
       "\<N>",
       "\<O>",
       "\<P>",
       "\<Q>",
       "\<R>",
       "\<S>",
       "\<T>",
       "\<U>",
       "\<V>",
       "\<W>",
       "\<X>",
       "\<Y>",
       "\<Z>",
       "\<a>",
       "\<b>",
       "\<c>",
       "\<d>",
       "\<e>",
       "\<f>",
       "\<g>",
       "\<h>",
       "\<i>",
       "\<j>",
       "\<k>",
       "\<l>",
       "\<m>",
       "\<n>",
       "\<o>",
       "\<p>",
       "\<q>",
       "\<r>",
       "\<s>",
       "\<t>",
       "\<u>",
       "\<v>",
       "\<w>",
       "\<x>",
       "\<y>",
       "\<z>",
       "\<AA>",
       "\<BB>",
       "\<CC>",
       "\<DD>",
       "\<EE>",
       "\<FF>",
       "\<GG>",
       "\<HH>",
       "\<II>",
       "\<JJ>",
       "\<KK>",
       "\<LL>",
       "\<MM>",
       "\<NN>",
       "\<OO>",
       "\<PP>",
       "\<QQ>",
       "\<RR>",
       "\<SS>",
       "\<TT>",
       "\<UU>",
       "\<VV>",
       "\<WW>",
       "\<XX>",
       "\<YY>",
       "\<ZZ>",
       "\<aa>",
       "\<bb>",
       "\<cc>",
       "\<dd>",
       "\<ee>",
       "\<ff>",
       "\<gg>",
       "\<hh>",
       "\<ii>",
       "\<jj>",
       "\<kk>",
       "\<ll>",
       "\<mm>",
       "\<nn>",
       "\<oo>",
       "\<pp>",
       "\<qq>",
       "\<rr>",
       "\<ss>",
       "\<tt>",
       "\<uu>",
       "\<vv>",
       "\<ww>",
       "\<xx>",
       "\<yy>",
       "\<zz>",
       "\<alpha>",
       "\<beta>",
       "\<gamma>",
       "\<delta>",
       "\<epsilon>",
       "\<zeta>",
       "\<eta>",
       "\<theta>",
       "\<iota>",
       "\<kappa>",
       (*"\<lambda>", sic!*)
       "\<mu>",
       "\<nu>",
       "\<xi>",
       "\<pi>",
       "\<rho>",
       "\<sigma>",
       "\<tau>",
       "\<upsilon>",
       "\<phi>",
       "\<chi>",
       "\<psi>",
       "\<omega>",
       "\<Gamma>",
       "\<Delta>",
       "\<Theta>",
       "\<Lambda>",
       "\<Xi>",
       "\<Pi>",
       "\<Sigma>",
       "\<Upsilon>",
       "\<Phi>",
       "\<Psi>",
       "\<Omega>"
     ];
 in
 
 val is_letter_symbol = Symtab.defined letter_symbols;
 
 end;
 
 datatype kind = Letter | Digit | Quasi | Blank | Other;
 
 fun kind s =
   if is_ascii_letter s then Letter
   else if is_ascii_digit s then Digit
   else if is_ascii_quasi s then Quasi
   else if is_ascii_blank s then Blank
   else if is_char s then Other
   else if is_letter_symbol s then Letter
   else Other;
 
 fun is_letter s = kind s = Letter;
 fun is_digit s = kind s = Digit;
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
 val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
+val has_block_ctrl = exists is_block_ctrl;
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 
 
 (* escape *)
 
 val esc = fn s =>
   if is_char s then s
   else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
   else "\\" ^ s;
 
 val escape = implode o map esc o Symbol.explode;
 
 
 
 (** scanning through symbols **)
 
 (* scanner *)
 
 fun scanner msg scan syms =
   let
     fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
       | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));
     val finite_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
     (case finite_scan syms of
       (result, []) => result
     | (_, rest) => error (message (rest, NONE) ()))
   end;
 
 
 (* space-separated words *)
 
 val scan_word =
   Scan.many1 is_ascii_blank >> K NONE ||
   Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
 
 val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
 
 val explode_words = split_words o Symbol.explode;
 
 
 (* blanks *)
 
 val trim_blanks = Symbol.explode #> trim is_blank #> implode;
 
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\<^sub>" :: _) = true
   | symbolic_end ("'" :: ss) = symbolic_end ss
   | symbolic_end (s :: _) = raw_symbolic s
   | symbolic_end [] = false;
 
 fun bump_init str =
   if symbolic_end (rev (Symbol.explode str)) then str ^ "'"
   else str ^ "a";
 
 fun bump_string str =
   let
     fun bump [] = ["a"]
       | bump ("z" :: ss) = "a" :: bump ss
       | bump (s :: ss) =
           if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z"
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
     val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;
 
 
 (* styles *)
 
 val sub = "\092<^sub>";
 val sup = "\092<^sup>";
 val bold = "\092<^bold>";
 
 fun make_style sym =
   Symbol.explode #> maps (fn s => [sym, s]) #> implode;
 
 val make_sub = make_style sub;
 val make_sup = make_style sup;
 val make_bold = make_style bold;
 
 
 
 (** symbol output **)
 
 (* length *)
 
 fun sym_len s =
   if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
   else if is_printable s then 1
   else 0;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
 fun output s = (s, sym_length (Symbol.explode s));
 
 
 (*final declarations of this structure!*)
 val explode = Symbol.explode;
 val length = sym_length;
 
 end;
diff --git a/src/Pure/Syntax/lexicon.ML b/src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML
+++ b/src/Pure/Syntax/lexicon.ML
@@ -1,487 +1,496 @@
 (*  Title:      Pure/Syntax/lexicon.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Lexer for the inner Isabelle syntax (terms and types).
 *)
 
 signature LEXICON =
 sig
   structure Syntax:
   sig
     val const: string -> term
     val free: string -> term
     val var: indexname -> term
   end
   val scan_id: Symbol_Pos.T list scanner
   val scan_longid: Symbol_Pos.T list scanner
   val scan_tid: Symbol_Pos.T list scanner
   val scan_hex: Symbol_Pos.T list scanner
   val scan_bin: Symbol_Pos.T list scanner
   val scan_var: Symbol_Pos.T list scanner
   val scan_tvar: Symbol_Pos.T list scanner
   val is_tid: string -> bool
   datatype token_kind =
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
     String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
   eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
   val end_pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val dummy: token
   val literal: string -> token
   val is_literal: token -> bool
   val tokens_match_ord: token ord
   val mk_eof: Position.T -> token
   val eof: token
   val is_eof: token -> bool
   val stopper: token Scan.stopper
   val terminals: string list
   val is_terminal: string -> bool
   val get_terminal: string -> token option
-  val literal_markup: string -> Markup.T
-  val report_of_token: token -> Position.report
+  val suppress_literal_markup: string -> bool
+  val suppress_markup: token -> bool
+  val literal_markup: string -> Markup.T list
+  val reports_of_token: token -> Position.report list
   val reported_token_range: Proof.context -> token -> string
   val valued_token: token -> bool
   val implode_string: Symbol.symbol list -> string
   val explode_string: string * Position.T -> Symbol_Pos.T list
   val implode_str: Symbol.symbol list -> string
   val explode_str: string * Position.T -> Symbol_Pos.T list
   val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
   val read_nat: string -> int option
   val read_int: string -> int option
   val read_num: string -> {radix: int, leading_zeros: int, value: int}
   val read_float: string -> {mant: int, exp: int}
   val mark_class: string -> string val unmark_class: string -> string
   val mark_type: string -> string val unmark_type: string -> string
   val mark_const: string -> string val unmark_const: string -> string
   val mark_fixed: string -> string val unmark_fixed: string -> string
   val unmark:
    {case_class: string -> 'a,
     case_type: string -> 'a,
     case_const: string -> 'a,
     case_fixed: string -> 'a,
     case_default: string -> 'a} -> string -> 'a
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
 end;
 
 structure Lexicon: LEXICON =
 struct
 
 (** syntactic terms **)
 
 structure Syntax =
 struct
 
 fun const c = Const (c, dummyT);
 fun free x = Free (x, dummyT);
 fun var xi = Var (xi, dummyT);
 
 end;
 
 
 
 (** basic scanners **)
 
 open Basic_Symbol_Pos;
 
 val err_prefix = "Inner lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 val scan_id = Symbol_Pos.scan_ident;
 val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
 val scan_tid = $$$ "'" @@@ scan_id;
 
 val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 val scan_num = scan_hex || scan_bin || Symbol_Pos.scan_nat;
 
 val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ Symbol_Pos.scan_nat) [];
 val scan_var = $$$ "?" @@@ scan_id_nat;
 val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
 
 fun is_tid s =
   (case try (unprefix "'") s of
     SOME s' => Symbol_Pos.is_identifier s'
   | NONE => false);
 
 
 
 (** tokens **)
 
 (* datatype token_kind *)
 
 datatype token_kind =
   Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
   String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
 
 val token_kinds =
   Vector.fromList
    [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
     String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
     Comment Comment.Latex, Dummy, EOF];
 
 fun token_kind i = Vector.sub (token_kinds, i);
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
 
 
 (* datatype token *)
 
 datatype token = Token of int * string * Position.range;
 
 fun index_of_token (Token (i, _, _)) = i;
 val kind_of_token = index_of_token #> token_kind;
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
 fun end_pos_of_token (Token (_, _, (_, end_pos))) = end_pos;
 
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 val dummy = Token (token_kind_index Dummy, "", Position.no_range);
 
 
 (* literals *)
 
 val literal_index = token_kind_index Literal;
 fun literal s = Token (literal_index, s, Position.no_range);
 fun is_literal tok = index_of_token tok = literal_index;
 
 fun tokens_match_ord toks =
   let val is = apply2 index_of_token toks in
     (case int_ord is of
       EQUAL => if #1 is = literal_index then fast_string_ord (apply2 str_of_token toks) else EQUAL
     | ord => ord)
   end;
 
 
 (* stopper *)
 
 val eof_index = token_kind_index EOF;
 fun mk_eof pos = Token (eof_index, "", (pos, Position.none));
 val eof = mk_eof Position.none;
 
 fun is_eof tok = index_of_token tok = eof_index;
 val stopper = Scan.stopper (K eof) is_eof;
 
 
 (* terminal symbols *)
 
 val terminal_symbols =
   [("id", Ident),
    ("longid", Long_Ident),
    ("var", Var),
    ("tid", Type_Ident),
    ("tvar", Type_Var),
    ("num_token", Num),
    ("float_token", Float),
    ("str_token", Str),
    ("string_token", String),
    ("cartouche", Cartouche)]
   |> map (apsnd token_kind_index)
   |> Symtab.make;
 
 val terminals = Symtab.keys terminal_symbols;
 val is_terminal = Symtab.defined terminal_symbols;
 fun get_terminal s =
   (case Symtab.lookup terminal_symbols s of
     SOME i => SOME (Token (i, s, Position.no_range))
   | NONE => NONE);
 
 
 (* markup *)
 
+val suppress_literal_markup = Symbol.has_block_ctrl o Symbol.explode;
+fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
+
 fun literal_markup s =
-  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
-  then Markup.literal
-  else Markup.delimiter;
+  let val syms = Symbol.explode s in
+    if Symbol.has_block_ctrl syms then []
+    else if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter syms
+    then [Markup.literal]
+    else [Markup.delimiter]
+  end;
 
 val token_kind_markup =
- fn Type_Ident => Markup.tfree
-  | Type_Var => Markup.tvar
-  | Num => Markup.numeral
-  | Float => Markup.numeral
-  | Str => Markup.inner_string
-  | String => Markup.inner_string
-  | Cartouche => Markup.inner_cartouche
-  | Comment _ => Markup.comment1
-  | _ => Markup.empty;
+ fn Type_Ident => [Markup.tfree]
+  | Type_Var => [Markup.tvar]
+  | Num => [Markup.numeral]
+  | Float => [Markup.numeral]
+  | Str => [Markup.inner_string]
+  | String => [Markup.inner_string]
+  | Cartouche => [Markup.inner_cartouche]
+  | Comment _ => [Markup.comment1]
+  | _ => [];
 
-fun report_of_token tok =
+fun reports_of_token tok =
   let
-    val markup =
+    val pos = pos_of_token tok;
+    val markups =
       if is_literal tok then literal_markup (str_of_token tok)
       else token_kind_markup (kind_of_token tok);
-  in (pos_of_token tok, markup) end;
+  in map (pair pos) markups end;
 
 fun reported_token_range ctxt tok =
   if is_proper tok
   then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
   else "";
 
 
 (* valued_token *)
 
 fun valued_token tok =
   not (is_literal tok orelse is_eof tok);
 
 
 
 (** string literals **)
 
 fun explode_literal scan_body (str, pos) =
   (case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of
     SOME ss => ss
   | _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos));
 
 
 (* string *)
 
 val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2;
 val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2);
 
 fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss));
 val explode_string = explode_literal scan_string_body;
 
 
 (* str *)
 
 val scan_chr =
   $$ "\\" |-- $$$ "'" ||
   Scan.one
     ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o
       Symbol_Pos.symbol) >> single ||
   $$$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
   Scan.ahead ($$ "'" -- $$ "'") |--
     !!! "unclosed string literal"
       ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'");
 
 val scan_str_body =
   Scan.ahead ($$ "'" |-- $$ "'") |--
     !!! "unclosed string literal"
       ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'");
 
 fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
 val explode_str = explode_literal scan_str_body;
 
 
 
 (** tokenize **)
 
 val token_leq = op <= o apply2 str_of_token;
 
 fun token kind =
   let val i = token_kind_index kind
   in fn ss => Token (i, Symbol_Pos.content ss, Symbol_Pos.range ss) end;
 
 fun tokenize lex xids syms =
   let
     val scan_xid =
       (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
       $$$ "_" @@@ $$$ "_";
 
     val scan_val =
       scan_tvar >> token Type_Var ||
       scan_var >> token Var ||
       scan_tid >> token Type_Ident ||
       Symbol_Pos.scan_float >> token Float ||
       scan_num >> token Num ||
       scan_longid >> token Long_Ident ||
       scan_xid >> token Ident;
 
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
       Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
       Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in
     (case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan)) syms of
       (toks, []) => toks
     | (_, ss) =>
         error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^
           Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss))))
   end;
 
 
 
 (** scan variables **)
 
 (* scan_indexname *)
 
 local
 
 val scan_vname =
   let
     fun nat n [] = n
       | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs;
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
       | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
 
     val scan =
       (scan_id >> map Symbol_Pos.symbol) --
       Scan.optional ($$ "." |-- Symbol_Pos.scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>
       (fn (cs, ~1) => chop_idx (rev cs) []
         | (cs, i) => (implode cs, i))
   end;
 
 in
 
 val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
 
 end;
 
 
 (* indexname *)
 
 fun read_indexname s =
   (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of
     SOME xi => xi
   | _ => error ("Lexical error in variable name: " ^ quote s));
 
 
 (* read_var *)
 
 fun read_var str =
   let
     val scan =
       $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
         >> Syntax.var ||
       Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
         >> (Syntax.free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end;
 
 
 (* read_variable *)
 
 fun read_variable str =
   let val scan = $$ "?" |-- scan_indexname || scan_indexname
   in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end;
 
 
 (* read numbers *)
 
 local
 
 fun nat cs =
   Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
     (Scan.read Symbol_Pos.stopper Symbol_Pos.scan_nat cs);
 
 in
 
 fun read_nat s = nat (Symbol_Pos.explode0 s);
 
 fun read_int s =
   (case Symbol_Pos.explode0 s of
     ("-", _) :: cs => Option.map ~ (nat cs)
   | cs => nat cs);
 
 end;
 
 
 (* read_num: hex/bin/decimal *)
 
 local
 
 val ten = Char.ord #"0" + 10;
 val a = Char.ord #"a";
 val A = Char.ord #"A";
 val _ = a > A orelse raise Fail "Bad ASCII";
 
 fun remap_hex c =
   let val x = ord c in
     if x >= a then chr (x - a + ten)
     else if x >= A then chr (x - A + ten)
     else c
   end;
 
 fun leading_zeros ["0"] = 0
   | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
   | leading_zeros _ = 0;
 
 in
 
 fun read_num str =
   let
     val (radix, digs) =
       (case Symbol.explode str of
         "0" :: "x" :: cs => (16, map remap_hex cs)
       | "0" :: "b" :: cs => (2, cs)
       | cs => (10, cs));
   in
    {radix = radix,
     leading_zeros = leading_zeros digs,
     value = #1 (Library.read_radix_int radix digs)}
   end;
 
 end;
 
 fun read_float str =
   let
     val cs = Symbol.explode str;
     val (intpart, fracpart) =
       (case chop_prefix Symbol.is_digit cs of
         (intpart, "." :: fracpart) => (intpart, fracpart)
       | _ => raise Fail "read_float");
   in
    {mant = #1 (Library.read_int (intpart @ fracpart)),
     exp = length fracpart}
   end;
 
 
 (* marked logical entities *)
 
 fun marker s = (prefix s, unprefix s);
 
 val (mark_class, unmark_class) = marker "\<^class>";
 val (mark_type, unmark_type) = marker "\<^type>";
 val (mark_const, unmark_const) = marker "\<^const>";
 val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
 
 fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
   (case try unmark_class s of
     SOME c => case_class c
   | NONE =>
       (case try unmark_type s of
         SOME c => case_type c
       | NONE =>
           (case try unmark_const s of
             SOME c => case_const c
           | NONE =>
               (case try unmark_fixed s of
                 SOME c => case_fixed c
               | NONE => case_default s))));
 
 val is_marked =
   unmark {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
 val dummy_type = Syntax.const (mark_type "dummy");
 val fun_type = Syntax.const (mark_type "fun");
 
 
 (* toplevel pretty printing *)
 
 val _ =
   ML_system_pp (fn _ => fn _ =>
     Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;
diff --git a/src/Pure/Syntax/printer.ML b/src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML
+++ b/src/Pure/Syntax/printer.ML
@@ -1,307 +1,307 @@
 (*  Title:      Pure/Syntax/printer.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Pretty printing of asts, terms, types and print (ast) translation.
 *)
 
 signature BASIC_PRINTER =
 sig
   val show_brackets: bool Config.T
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
 end;
 
 signature PRINTER =
 sig
   include BASIC_PRINTER
   val show_markup_default: bool Unsynchronized.ref
   val show_type_emphasis: bool Config.T
   val type_emphasis: Proof.context -> typ -> bool
   type prtabs
   datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
   val get_prefix: prtabs -> Symtab.key -> string option
   val get_binder: prtabs -> Symtab.key -> string option
   val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> Ast.ast list -> Pretty.T option) ->
     (string -> Markup.T list * string) ->
     Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> Ast.ast list -> Pretty.T option) ->
     (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
 struct
 
 (** options for printing **)
 
 val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
 val show_types = Config.declare_option_bool ("show_types", \<^here>);
 val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
 val show_markup_default = Unsynchronized.ref false;
 val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
 val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false);
 val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>);
 val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true);
 
 fun type_emphasis ctxt T =
   T <> dummyT andalso
     (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
       Config.get ctxt show_type_emphasis andalso not (is_Type T));
 
 
 
 (** type prtabs **)
 
 datatype symb =
   Arg of int |
   TypArg of int |
   String of bool * string |
   Break of int |
   Block of Syntax_Ext.block_info * symb list;
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
 fun mode_tab (prtabs: prtabs) mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
 fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
 
 fun lookup_default prtabs = Symtab.lookup_list (mode_tab prtabs "");
 
 
 (* approximative syntax *)
 
 datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
 
 local
 
 fun is_arg (Arg _) = true
   | is_arg (TypArg _) = true
   | is_arg _ = false;
 
 fun is_space str = forall_string (fn s => s = " ") str;
 
 fun clean symbs = symbs |> maps
   (fn Block (_, body) => clean body
     | symb as String (_, s) => if is_space s then [] else [symb]
     | symb => if is_arg symb then [symb] else []);
 
 in
 
 fun get_prefix prtabs c =
   lookup_default prtabs c
   |> get_first (fn (symbs, _, _) =>
       (case clean symbs of
         String (_, d) :: rest => if forall is_arg rest then SOME d else NONE
       | _ => NONE));
 
 fun get_binder prtabs c =
   lookup_default prtabs (Mixfix.binder_name c)
   |> get_first (fn (symbs, _, _) =>
       (case clean symbs of
         String (_, d) :: _ => SOME d
       | _ => NONE));
 
 fun get_infix prtabs c =
   lookup_default prtabs c
   |> map_filter (fn (symbs, _, p) =>
       (case clean symbs of
         [Arg p1, String (_, d), Arg p2] => SOME (p1, p2, d, p)
       | [TypArg p1, String (_, d), TypArg p2] => SOME (p1, p2, d, p)
       | _ => NONE))
   |> get_first (fn (p1, p2, d, p) =>
       if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
       else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = d, pri = p}
       else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
       else NONE);
 
 end;
 
 
 (* xprod_to_fmt *)
 
 fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
   | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
       let
         fun arg (s, p) =
           (if s = "type" then TypArg else Arg)
           (if Lexicon.is_terminal s then 1000 else p);
 
         fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
-              apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s)))
+              apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
                 (xsyms_to_syms xsyms)
           | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
               apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
               apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Syntax_Ext.Bg info :: xsyms) =
               let
                 val (bsyms, xsyms') = xsyms_to_syms xsyms;
                 val (syms, xsyms'') = xsyms_to_syms xsyms';
               in
                 (Block (info, bsyms) :: syms, xsyms'')
               end
           | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
               apfst (cons (Break i)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
           | xsyms_to_syms [] = ([], []);
 
         fun nargs (Arg _ :: syms) = nargs syms + 1
           | nargs (TypArg _ :: syms) = nargs syms + 1
           | nargs (String _ :: syms) = nargs syms
           | nargs (Break _ :: syms) = nargs syms
           | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
           | nargs [] = 0;
       in
         (case xsyms_to_syms xsymbs of
           (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
         | _ => raise Fail "Unbalanced pretty-printing blocks")
       end;
 
 
 (* empty, extend, merge prtabs *)
 
 val empty_prtabs = [];
 
 fun update_prtabs mode xprods prtabs =
   let
     val fmts = map_filter xprod_to_fmt xprods;
     val tab' = fold (Symtab.update_list (op =)) fmts (mode_tab prtabs mode);
   in AList.update (op =) (mode, tab') prtabs end;
 
 fun remove_prtabs mode xprods prtabs =
   let
     val tab = mode_tab prtabs mode;
     val fmts = map_filter (fn xprod as Syntax_Ext.XProd (_, _, c, _) =>
       if null (Symtab.lookup_list tab c) then NONE
       else xprod_to_fmt xprod) xprods;
     val tab' = fold (Symtab.remove_list (op =)) fmts tab;
   in AList.update (op =) (mode, tab') prtabs end;
 
 fun merge_prtabs prtabs1 prtabs2 =
   let
     val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
     fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   in map merge modes end;
 
 
 
 (** pretty term or typ asts **)
 
 fun is_chain [Block (_, pr)] = is_chain pr
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
 val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
 
 fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
   let
     val show_brackets = Config.get ctxt show_brackets;
 
     (*default applications: prefix / postfix*)
     val appT =
       if type_mode then Syntax_Trans.tappl_ast_tr'
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 
     fun synT _ ([], args) = ([], args)
       | synT m (Arg p :: symbs, t :: args) =
           let val (Ts, args') = synT m (symbs, args);
           in (astT (t, p) @ Ts, args') end
       | synT m (TypArg p :: symbs, t :: args) =
           let
             val (Ts, args') = synT m (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
             else
               (pretty true curried (Config.put pretty_priority p ctxt)
                 tabs trf markup_trans markup_extern t @ Ts, args')
           end
       | synT m (String (do_mark, s) :: symbs, args) =
           let
             val (Ts, args') = synT m (symbs, args);
             val T =
               if do_mark
-              then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
+              then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
               else Pretty.str s;
           in (T :: Ts, args') end
       | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
           let
             val (bTs, args') = synT m (bsymbs, args);
             val (Ts, args'') = synT m (symbs, args');
             val T =
               Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs
               |> unbreakable ? Pretty.unbreakable;
           in (T :: Ts, args'') end
       | synT m (Break i :: symbs, args) =
           let
             val (Ts, args') = synT m (symbs, args);
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
           in (T :: Ts, args') end
 
     and parT m (pr, args, p, p': int) = #1 (synT m
           (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
             [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
            else pr, args))
 
     and atomT a = Pretty.marks_str (markup_extern a)
 
     and prefixT (_, a, [], _) = [atomT a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
 
     and splitT 0 ([x], ys) = (x, ys)
       | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
       | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
 
     and combT (tup as (c, a, args, p)) =
       let
         val nargs = length args;
 
         (*find matching table entry, or print as prefix / postfix*)
         fun prnt ([], []) = prefixT tup
           | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
           | prnt ((pr, n, p') :: prnps, tbs) =
               if nargs = n then parT (#1 (markup_extern a)) (pr, args, p, p')
               else if nargs > n andalso not type_mode then
                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
       in
         (case markup_trans a args of
           SOME prt => [prt]
         | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
       end
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
       | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast]
       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
       | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
   in astT (ast0, Config.get ctxt pretty_priority) end;
 
 
 (* pretty_term_ast *)
 
 fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast =
   pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
 
 
 (* pretty_typ_ast *)
 
 fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast =
   pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
 
 end;
 
 structure Basic_Printer: BASIC_PRINTER = Printer;
 open Basic_Printer;
 
diff --git a/src/Pure/Syntax/syntax_phases.ML b/src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML
+++ b/src/Pure/Syntax/syntax_phases.ML
@@ -1,1017 +1,1021 @@
 (*  Title:      Pure/Syntax/syntax_phases.ML
     Author:     Makarius
 
 Main phases of inner syntax processing, with standard implementations
 of parse/unparse operations.
 *)
 
 signature SYNTAX_PHASES =
 sig
   val reports_of_scope: Position.T list -> Position.report list
   val decode_sort: term -> sort
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
     Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
   val print_checks: Proof.context -> unit
   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
   val term_check: int -> string -> (Proof.context -> term list -> term list) ->
     Context.generic -> Context.generic
   val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
   val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
     Context.generic -> Context.generic
   val typ_check': int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val term_check': int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
   val typ_uncheck': int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val term_uncheck': int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
 struct
 
 (** markup logical entities **)
 
 fun markup_class ctxt c =
   [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_type ctxt c =
   [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_const ctxt c =
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
   Variable.markup ctxt x ::
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
 fun markup_bound def ps (name, id) =
   let val entity = Markup.entity Markup.boundN name in
     Markup.bound ::
       map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
   end;
 
 fun markup_entity ctxt c =
   (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
     SOME "" => []
   | SOME b => markup_entity ctxt b
   | NONE => c |> Lexicon.unmark
      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
       case_fixed = markup_free ctxt,
       case_default = K []});
 
 
 
 (** reports of implicit variable scope **)
 
 fun reports_of_scope [] = []
   | reports_of_scope (def_pos :: ps) =
       let
         val id = serial ();
         fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
       in
         map (rpair Markup.bound) (def_pos :: ps) @
         ((def_pos, entity true) :: map (rpair (entity false)) ps)
       end;
 
 
 
 (** decode parse trees **)
 
 (* decode_sort *)
 
 fun decode_sort tm =
   let
     fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
 
     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
 
     fun classes (Const (s, _)) = [class s]
       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
       | classes _ = err ();
 
     fun sort (Const ("_dummy_sort", _)) = dummyS
       | sort (Const ("_topsort", _)) = []
       | sort (Const ("_sort", _) $ cs) = classes cs
       | sort (Const (s, _)) = [class s]
       | sort _ = err ();
   in sort tm end;
 
 
 (* decode_typ *)
 
 fun decode_pos (Free (s, _)) =
       if is_some (Term_Position.decode s) then SOME s else NONE
   | decode_pos _ = NONE;
 
 fun decode_typ tm =
   let
     fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
 
     fun typ ps sort tm =
       (case tm of
         Const ("_tfree", _) $ t => typ ps sort t
       | Const ("_tvar", _) $ t => typ ps sort t
       | Const ("_ofsort", _) $ t $ s =>
           (case decode_pos s of
             SOME p => typ (p :: ps) sort t
           | NONE =>
               if is_none sort then typ ps (SOME (decode_sort s)) t
               else err ())
       | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s)
       | Free (x, _) => TFree (x, ps @ the_default dummyS sort)
       | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort)
       | _ =>
           if null ps andalso is_none sort then
             let
               val (head, args) = Term.strip_comb tm;
               val a =
                 (case head of
                   Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
                 | _ => err ());
             in Type (a, map (typ [] NONE) args) end
           else err ());
   in typ [] NONE tm end;
 
 
 (* parsetree_to_ast *)
 
 fun parsetree_to_ast ctxt trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report pos = Position.store_reports reports [pos];
     val append_reports = Position.append_reports reports;
 
+    fun report_pos tok =
+      if Lexicon.suppress_markup tok then Position.none
+      else Lexicon.pos_of_token tok;
+
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => f ctxt args);
 
     fun asts_of_token tok =
       if Lexicon.valued_token tok
       then [Ast.Variable (Lexicon.str_of_token tok)]
       else [];
 
     fun ast_of_position tok =
-      Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
+      Ast.Variable (Term_Position.encode (report_pos tok));
 
     fun ast_of_dummy a tok =
       Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
 
     fun asts_of_position c tok =
       [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
     and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
           let
-            val pos = Lexicon.pos_of_token tok;
+            val pos = report_pos tok;
             val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
-            val pos = Lexicon.pos_of_token tok;
+            val pos = report_pos tok;
             val (Type (c, _), rs) =
               Proof_Context.check_type_name {proper = true, strict = false} ctxt
                 (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
       | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
           [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
       | asts_of (Parser.Node (a, pts)) =
           let
             val _ = pts |> List.app
               (fn Parser.Node _ => () | Parser.Tip tok =>
                 if Lexicon.valued_token tok then ()
-                else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
+                else report (report_pos tok) (markup_entity ctxt) a);
           in [trans a (maps asts_of pts)] end
       | asts_of (Parser.Tip tok) = asts_of_token tok
 
     and ast_of pt =
       (case asts_of pt of
         [ast] => ast
       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
 
     val ast = Exn.interruptible_capture ast_of parsetree;
   in (! reports, ast) end;
 
 
 (* ast_to_term *)
 
 fun ast_to_term ctxt trf =
   let
     fun trans a args =
       (case trf a of
         NONE => Term.list_comb (Syntax.const a, args)
       | SOME f => f ctxt args);
 
     fun term_of (Ast.Constant a) = trans a []
       | term_of (Ast.Variable x) = Lexicon.read_var x
       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
           trans a (map term_of asts)
       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   in term_of end;
 
 
 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_const ctxt (c, ps) =
   let
     val (Const (c', _), reports) =
       Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps);
   in (c', reports) end;
 
 local
 
 fun get_free ctxt x =
   let
     val fixed = Variable.lookup_fixed ctxt x;
     val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
     val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   in
     if Variable.is_const ctxt x then NONE
     else if is_some fixed then fixed
     else if not is_const orelse is_declared then SOME x
     else NONE
   end;
 
 in
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
         val reports = Unsynchronized.ref reports0;
         fun report ps = Position.store_reports reports ps;
         val append_reports = Position.append_reports reports;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
               | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
               | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
               let
                 val id = serial ();
                 val _ = report qs (markup_bound true qs) (x, id);
               in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
           | decode ps _ _ (Const (a, T)) =
               (case try Lexicon.unmark_fixed a of
                 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
               | NONE =>
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
                         SOME c => c
                       | NONE => #1 (decode_const ctxt (a, [])));
                     val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
               ((Name.reject_internal (a, ps) handle ERROR msg =>
                   error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
                 (case get_free ctxt a of
                   SOME x => (report ps (markup_free ctxt) x; Free (x, T))
                 | NONE =>
                     let
                       val (c, rs) = decode_const ctxt (a, ps);
                       val _ = append_reports rs;
                     in Const (c, T) end))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
                 SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
               | NONE => t);
 
         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
 end;
 
 
 
 (** parse **)
 
 (* results *)
 
 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
 
 fun report_result ctxt pos ambig_msgs results =
   (case (proper_results results, failed_results results) of
     ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn)
   | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
   | _ =>
       if null ambig_msgs then
         error ("Parse error: ambiguous syntax" ^ Position.here pos)
       else error (cat_lines ambig_msgs));
 
 
 (* parse raw asts *)
 
 fun parse_asts ctxt raw root (syms, pos) =
   let
     val syn = Proof_Context.syn_of ctxt;
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
-    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
+    val _ = Context_Position.reports ctxt (maps Lexicon.reports_of_token toks);
 
     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
         error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
     val len = length pts;
 
     val limit = Config.get ctxt Syntax.ambiguity_limit;
     val ambig_msgs =
       if len <= 1 then []
       else
         [cat_lines
           (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
             " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
               (take limit pts))];
 
   in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
 
 fun parse_tree ctxt root input =
   let
     val syn = Proof_Context.syn_of ctxt;
     val tr = Syntax.parse_translation syn;
     val parse_rules = Syntax.parse_rules syn;
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
     val results =
       (map o apsnd o Exn.maps_res)
         (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
 
 (* parse logical entities *)
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
 
 fun parse_sort ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_sort
       |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_typ
       handle ERROR msg => parse_failed ctxt pos msg "type");
 
 fun parse_term is_prop ctxt =
   let
     val (markup, kind, root, constrain) =
       if is_prop
       then (Markup.language_prop, "prop", "prop", Type.constraint propT)
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term (Proof_Context.consts_of ctxt);
   in
     Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
           val parsed_len = length (proper_results results);
 
           val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
           val limit = Config.get ctxt Syntax.ambiguity_limit;
 
           (*brute-force disambiguation via type-inference*)
           fun check t =
             (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t)
               handle exn as ERROR _ => Exn.Exn exn;
 
           val results' =
             if parsed_len > 1 then
               (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res)
                 check results
             else results;
           val reports' = fst (hd results');
 
           val errs = map snd (failed_results results');
           val checked = map snd (proper_results results');
           val checked_len = length checked;
 
           val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
         in
           if checked_len = 0 then
             report_result ctxt pos []
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
           else if checked_len = 1 then
             (if not (null ambig_msgs) andalso ambiguity_warning andalso
                 Context_Position.is_visible ctxt then
               warning
                 (cat_lines (ambig_msgs @
                   ["Fortunately, only one parse tree is well-formed and type-correct,\n\
                    \but you may still want to disambiguate your grammar or your input."]))
              else (); report_result ctxt pos [] results')
           else
             report_result ctxt pos []
               [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
                 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
                   (if checked_len <= limit then ""
                    else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
                   map (Pretty.string_of o Pretty.item o single o pretty_term)
                     (take limit checked))))))]
         end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;
 
 
 (* parse_ast_pattern *)
 
 fun parse_ast_pattern ctxt (root, str) =
   let
     val syn = Proof_Context.syn_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report ps = Position.store_reports reports ps;
 
     fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
     fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
     fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
     and decode ps (Ast.Constant c) = decode_const ps c
       | decode ps (Ast.Variable x) =
           if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
           then decode_const ps x
           else decode_var ps x
       | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
           if member (op =) Term_Position.markers c then
             (case Term_Position.decode x of
               SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
             | NONE => decode_appl ps asts)
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
     val source = Syntax.read_input str;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;
 
 
 
 (** encode parse trees **)
 
 (* term_of_sort *)
 
 fun term_of_sort S =
   let
     val class = Syntax.const o Lexicon.mark_class;
 
     fun classes [c] = class c
       | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
   in
     if S = dummyS then Syntax.const "_dummy_sort"
     else
       (case S of
         [] => Syntax.const "_topsort"
       | [c] => class c
       | cs => Syntax.const "_sort" $ classes cs)
   end;
 
 
 (* term_of_typ *)
 
 fun term_of_typ ctxt ty =
   let
     val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
 
     fun ofsort t raw_S =
       if show_sorts then
         let val S = #2 (Term_Position.decode_positionS raw_S)
         in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
       else t;
 
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
           if is_some (Term_Position.decode x) then Syntax.free x
           else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
       | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
   in term_of ty end;
 
 
 (* simple_ast_of *)
 
 fun simple_ast_of ctxt =
   let
     val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
     fun ast_of (Const (c, _)) = Ast.Constant c
       | ast_of (Free (x, _)) = Ast.Variable x
       | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
       | ast_of (t as _ $ _) =
           let val (f, args) = strip_comb t
           in Ast.mk_appl (ast_of f) (map ast_of args) end
       | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
       | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   in ast_of end;
 
 
 (* sort_to_ast and typ_to_ast *)
 
 fun ast_of_termT ctxt trf tm =
   let
     val ctxt' = Config.put show_sorts false ctxt;
     fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
       | ast_of (Const (a, _)) = trans a []
       | ast_of (t as _ $ _) =
           (case strip_comb t of
             (Const (a, _), args) => trans a args
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of ctxt t
     and trans a args = ast_of (trf a ctxt' dummyT args)
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
 
 
 (* term_to_ast *)
 
 local
 
 fun mark_aprop tm =
   let
     fun aprop t = Syntax.const "_aprop" $ t;
 
     fun is_prop Ts t =
       Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
         handle TERM _ => false;
 
     fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun mark _ (t as Const _) = t
       | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
       | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
       | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
       | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
       | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
       | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) =
           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
           else mark Ts t1 $ mark Ts t2
       | mark Ts (t as t1 $ t2) =
           (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
             (mark Ts t1 $ mark Ts t2);
   in mark [] tm end;
 
 fun prune_types tm =
   let
     fun regard t t' seen =
       if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
       else if member (op aconv) seen t then (t', seen)
       else (t, t :: seen);
 
     fun prune (t as Const _, seen) = (t, seen)
       | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
       | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
       | prune (t as Bound _, seen) = (t, seen)
       | prune (Abs (x, T, t), seen) =
           let val (t', seen') = prune (t, seen);
           in (Abs (x, T, t'), seen') end
       | prune (t1 $ t2, seen) =
           let
             val (t1', seen') = prune (t1, seen);
             val (t2', seen'') = prune (t2, seen');
           in (t1' $ t2', seen'') end;
   in #1 (prune (tm, [])) end;
 
 fun mark_atoms is_syntax_const ctxt tm =
   let
     val {structs, fixes} = Syntax_Trans.get_idents ctxt;
     val show_structs = Config.get ctxt show_structs;
 
     fun mark ((t as Const (c, _)) $ u) =
           if member (op =) Pure_Thy.token_markers c
           then t $ u else mark t $ mark u
       | mark (t $ u) = mark t $ mark u
       | mark (Abs (x, T, t)) = Abs (x, T, mark t)
       | mark (t as Const (c, T)) =
           if is_syntax_const c then t
           else Const (Lexicon.mark_const c, T)
       | mark (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
             if i = 0 andalso member (op =) fixes x then
               Const (Lexicon.mark_fixed x, T)
             else if i = 1 andalso not show_structs then
               Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
           if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;
 
 in
 
 fun term_to_ast is_syntax_const ctxt trf tm =
   let
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
 
     fun ast_of tm =
       (case strip_comb tm of
         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
       | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
           let
             val X =
               if show_markup andalso not show_types orelse B <> dummyT then T
               else dummyT;
           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
       | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args = ast_of (trf a ctxt T args)
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T0 =
       let
         val T =
           if show_markup andalso not show_types
           then Type_Annotation.clean T0
           else Type_Annotation.smash T0;
       in
         if (show_types orelse show_markup) andalso T <> dummyT then
           Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
             ast_of_termT ctxt trf (term_of_typ ctxt T)]
         else simple_ast_of ctxt t
       end;
   in
     tm
     |> mark_aprop
     |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
     |> mark_atoms is_syntax_const ctxt
     |> ast_of
   end;
 
 end;
 
 
 
 (** unparse **)
 
 local
 
 fun free_or_skolem ctxt x =
   let
     val m =
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
   in
     if Name.is_skolem x
     then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     else ([m, Markup.free], x)
   end;
 
 fun var_or_skolem s =
   (case Lexicon.read_variable s of
     SOME (x, i) =>
       (case try Name.dest_skolem x of
         NONE => (Markup.var, s)
       | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
   | NONE => (Markup.var, s));
 
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
     val show_types = Config.get ctxt show_types orelse show_sorts;
 
     val syn = Proof_Context.syn_of ctxt;
     val prtabs = Syntax.prtabs syn;
     val trf = Syntax.print_ast_translation syn;
 
     fun markup_extern c =
       (case Syntax.lookup_const syn c of
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
          {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
           case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
           case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,
           case_default = fn x => ([], x)});
 
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
       | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
       | token_trans _ _ = NONE;
 
     fun markup_trans a [Ast.Variable x] = token_trans a x
       | markup_trans "_constrain" [t, ty] = constrain_trans t ty
       | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
       | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s
       | markup_trans _ _ = NONE
 
     and constrain_trans t ty =
       if show_markup andalso not show_types then
         let
           val ((bg1, bg2), en) = typing_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end
       else NONE
 
     and ofsort_trans ty s =
       if show_markup andalso not show_sorts then
         let
           val ((bg1, bg2), en) = sorting_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end
       else NONE
 
     and pretty_typ_ast m ast = ast
       |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m
 
     and pretty_ast m ast = ast
       |> prt_t ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m;
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
     |> pretty_ast markup
   end;
 
 in
 
 val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
 
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val syn = Proof_Context.syn_of ctxt;
   in
     unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
       (Markup.language_term false) ctxt
   end;
 
 end;
 
 
 
 (** translations **)
 
 (* type propositions *)
 
 fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] =
       Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   | type_prop_tr' ctxt T [t] =
       Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
   | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
 
 
 (* type reflection *)
 
 fun type_tr' ctxt (Type ("itself", [T])) ts =
       Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
   | type_tr' _ _ _ = raise Match;
 
 
 (* type constraints *)
 
 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
       Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   | type_constraint_tr' _ _ _ = raise Match;
 
 
 (* authentic syntax *)
 
 fun const_ast_tr intern ctxt asts =
   (case asts of
     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
         val pos = the_default Position.none (Term_Position.decode p);
         val (c', _) = decode_const ctxt (c, [pos]);
         val d = if intern then Lexicon.mark_const c' else c;
       in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
   | _ => raise Ast.AST ("const_ast_tr", asts));
 
 
 (* setup translations *)
 
 val _ = Theory.setup
  (Sign.parse_ast_translation
    [("_context_const", const_ast_tr true),
     ("_context_xconst", const_ast_tr false)] #>
   Sign.typed_print_translation
    [("_type_prop", type_prop_tr'),
     ("\<^const>Pure.type", type_tr'),
     ("_type_constraint_", type_constraint_tr')]);
 
 
 
 (** check/uncheck **)
 
 (* context-sensitive (un)checking *)
 
 type key = int * bool;
 
 structure Checks = Generic_Data
 (
   type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
   type T =
     ((key * ((string * typ check) * stamp) list) list *
      (key * ((string * term check) * stamp) list) list);
   val empty = ([], []);
   val extend = I;
   fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
     (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
 );
 
 fun print_checks ctxt =
   let
     fun split_checks checks =
       List.partition (fn ((_, un), _) => not un) checks
       |> apply2 (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
           #> sort (int_ord o apply2 fst));
     fun pretty_checks kind checks =
       checks |> map (fn (i, names) => Pretty.block
         [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
           Pretty.brk 1, Pretty.strs names]);
 
     val (typs, terms) = Checks.get (Context.Proof ctxt);
     val (typ_checks, typ_unchecks) = split_checks typs;
     val (term_checks, term_unchecks) = split_checks terms;
   in
     pretty_checks "typ_checks" typ_checks @
     pretty_checks "term_checks" term_checks @
     pretty_checks "typ_unchecks" typ_unchecks @
     pretty_checks "term_unchecks" term_unchecks
   end |> Pretty.writeln_chunks;
 
 
 local
 
 fun context_check which (key: key) name f =
   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
 
 fun simple_check eq f xs ctxt =
   let val xs' = f ctxt xs
   in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
 
 in
 
 fun typ_check' stage = context_check apfst (stage, false);
 fun term_check' stage = context_check apsnd (stage, false);
 fun typ_uncheck' stage = context_check apfst (stage, true);
 fun term_uncheck' stage = context_check apsnd (stage, true);
 
 fun typ_check key name f = typ_check' key name (simple_check (op =) f);
 fun term_check key name f = term_check' key name (simple_check (op aconv) f);
 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
 
 end;
 
 
 local
 
 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
 fun check_all fs = perhaps_apply (map check_stage fs);
 
 fun check which uncheck ctxt0 xs0 =
   let
     val funs = which (Checks.get (Context.Proof ctxt0))
       |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
       |> Library.sort (int_ord o apply2 fst) |> map snd
       |> not uncheck ? map rev;
   in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
 
 val apply_typ_check = check fst false;
 val apply_term_check = check snd false;
 val apply_typ_uncheck = check fst true;
 val apply_term_uncheck = check snd true;
 
 in
 
 fun check_typs ctxt raw_tys =
   let
     val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
     val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
   in
     tys
     |> apply_typ_check ctxt
     |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
   end;
 
 fun check_terms ctxt raw_ts =
   let
     val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
     val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
 
     val tys = map (Logic.mk_type o snd) ps;
     val (ts', tys') = ts @ tys
       |> apply_term_check ctxt
       |> chop (length ts);
     val typing_report =
       fold2 (fn (pos, _) => fn ty =>
         if Position.is_reported pos then
           cons (Position.reported_text pos Markup.typing
             (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
         else I) ps tys' [];
 
     val _ =
       if Context_Position.reports_enabled ctxt
       then Output.report (sorting_report @ typing_report) else ();
   in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
 val uncheck_typs = apply_typ_uncheck;
 val uncheck_terms = apply_term_uncheck;
 
 end;
 
 
 (* install operations *)
 
 val _ =
   Theory.setup
    (Syntax.install_operations
      {parse_sort = parse_sort,
       parse_typ = parse_typ,
       parse_term = parse_term false,
       parse_prop = parse_term true,
       unparse_sort = unparse_sort,
       unparse_typ = unparse_typ,
       unparse_term = unparse_term,
       check_typs = check_typs,
       check_terms = check_terms,
       check_props = check_props,
       uncheck_typs = uncheck_typs,
       uncheck_terms = uncheck_terms});
 
 end;
 
 
 (* standard phases *)
 
 val _ = Context.>>
  (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
   Syntax_Phases.term_check 0 "standard"
     (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
   Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
   Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);