# HG changeset patch
# User wenzelm
# Date 1684865475 -7200
# Node ID 2cd7e5518d0d68d06a956cc5e8fe5f20cfeefb32
# Parent  2ea20bb1493caae095d3325172606d8ae9549ef5
clarified output of embedded values, e.g. for 'print_locale';

diff -r 2ea20bb1493c -r 2cd7e5518d0d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 23 19:12:21 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 23 20:11:15 2023 +0200
@@ -256,10 +256,10 @@
 in
 
 fun internal pos arg =
-  internal_source ("<attribute>", pos) (Token.Attribute (Morphism.entity arg));
+  internal_source ("internal", pos) (Token.Attribute (Morphism.entity arg));
 
 fun internal_declaration pos arg =
-  [([Drule.dummy_thm], [internal_source ("<declaration>", pos) (Token.Declaration arg)])];
+  [([Drule.dummy_thm], [internal_source ("declaration", pos) (Token.Declaration arg)])];
 
 end;
 
diff -r 2ea20bb1493c -r 2cd7e5518d0d src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue May 23 19:12:21 2023 +0200
+++ b/src/Pure/Isar/token.ML	Tue May 23 20:11:15 2023 +0200
@@ -558,6 +558,10 @@
 
 (* 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) =>
@@ -568,6 +572,8 @@
   | 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));