# HG changeset patch
# User wenzelm
# Date 1394461241 -3600
# Node ID 25889f5c39a8a6513dce381604a885224b7ab7c9
# Parent  893fe12639bc76381db98692f41c5d8bf0f926da
prefer Name_Space.pretty with its builtin markup;

diff -r 893fe12639bc -r 25889f5c39a8 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 15:04:01 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 15:20:41 2014 +0100
@@ -162,7 +162,7 @@
   let
     val ths = Attrib.eval_thms ctxt [xthm]
     val bracket =
-      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
+      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str ctxt) args
       |> implode
     fun nth_name j =
       (case xref of
diff -r 893fe12639bc -r 25889f5c39a8 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Mar 10 15:04:01 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Mar 10 15:20:41 2014 +0100
@@ -172,7 +172,7 @@
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
+  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str @{context}) args);
 
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
diff -r 893fe12639bc -r 25889f5c39a8 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 15:04:01 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 15:20:41 2014 +0100
@@ -10,7 +10,7 @@
   type src
   val src: (string * Token.T list) * Position.T -> src
   val dest_src: src -> (string * Token.T list) * Position.T
-  val pretty_src: Proof.context -> src -> Pretty.T
+  val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val transform_values: morphism -> src -> src
   val init_assignable: src -> src
@@ -79,7 +79,7 @@
 val src = Src;
 fun dest_src (Src src) = src;
 
-fun pretty_src ctxt src =
+fun pretty_src pretty_name ctxt src =
   let
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     fun prt arg =
@@ -90,8 +90,8 @@
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
       | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
       | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
-    val (s, args) = #1 (dest_src src);
-  in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
+    val (name, args) = #1 (dest_src src);
+  in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
 
 fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
 fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
diff -r 893fe12639bc -r 25889f5c39a8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 15:04:01 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 15:20:41 2014 +0100
@@ -109,6 +109,8 @@
     |> Pretty.chunks |> Pretty.writeln
   end;
 
+val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
+
 fun add_attribute name att comment thy = thy
   |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
 
@@ -129,12 +131,11 @@
 
 (* pretty printing *)
 
-fun extern ctxt =
-  Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
+fun pretty_attrib ctxt =
+  Args.pretty_src (Name_Space.pretty ctxt (attribute_space ctxt)) ctxt;
 
 fun pretty_attribs _ [] = []
-  | pretty_attribs ctxt srcs =
-      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
+  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (pretty_attrib ctxt) srcs)];
 
 
 (* get attributes *)
@@ -349,7 +350,7 @@
         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
-    val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
+    val space = attribute_space ctxt;
     val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;