src/Pure/Isar/token.ML

   | closure tok = tok;
 
 
 (* pretty *)
 
+fun pretty_keyword3 tok =
+  let val props = Position.properties_of (pos_of tok)
+  in Pretty.mark_str (Markup.properties props Markup.keyword3, unparse tok) end;
+
 fun pretty_value ctxt tok =
   (case get_value tok of
     SOME (Literal markup) =>
       let val x = content_of tok
       in Pretty.mark_str (keyword_markup markup x, x) end
   | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt))
   | SOME (Typ T) => Syntax.pretty_typ ctxt T
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
+  | SOME (Attribute _) => pretty_keyword3 tok
+  | SOME (Declaration _) => pretty_keyword3 tok
   | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
 
 
 (* src *)