# HG changeset patch
# User wenzelm
# Date 1160861150 -7200
# Node ID a56e6d1e56a3a5178d9b8d3e49ed24f03bff48c5
# Parent  8b21407de52624df555cb6a408da4aa8555e07e9
added pretty_attribs (from attrib.ML);

diff -r 8b21407de526 -r a56e6d1e56a3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Oct 14 23:25:48 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 14 23:25:50 2006 +0200
@@ -18,6 +18,7 @@
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
+  val pretty_attribs: Proof.context -> src list -> Pretty.T list
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
   val map_specs: ('a -> 'att) ->
@@ -79,11 +80,21 @@
 val print_attributes = AttributesData.print;
 
 
-(* interning *)
+(* name space *)
 
 val intern = NameSpace.intern o #1 o AttributesData.get;
 val intern_src = Args.map_name o intern;
 
+val extern = NameSpace.extern o #1 o AttributesData.get o ProofContext.theory_of;
+
+
+(* pretty printing *)
+
+fun pretty_attribs _ [] = []
+  | pretty_attribs ctxt srcs =
+      [Pretty.enclose "[" "]"
+        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+
 
 (* get attributes *)