# HG changeset patch
# User wenzelm
# Date 1477408925 -7200
# Node ID 5076725247faebf99e9343bfde09cdd9dd4fa982
# Parent  6e9c22c494c59956cfd8968a9e52886b8f8d9fdc
more robust printing of names in the context of outer syntax;

diff -r 6e9c22c494c5 -r 5076725247fa src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Oct 25 14:06:43 2016 +0200
+++ b/src/Pure/Isar/element.ML	Tue Oct 25 17:22:05 2016 +0200
@@ -127,13 +127,14 @@
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
     val prt_binding = Attrib.pretty_binding ctxt;
+    val prt_name = Proof_Context.pretty_name ctxt;
 
     fun prt_show (a, ts) =
       Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T, _) = Pretty.block
-          [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
-      | prt_var (x, NONE, _) = Pretty.str (Binding.name_of x);
+          [prt_name (Binding.name_of x), Pretty.str " ::", Pretty.brk 1, prt_typ T]
+      | prt_var (x, NONE, _) = prt_name (Binding.name_of x);
     val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
 
     fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props))
@@ -152,6 +153,7 @@
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
+    val prt_name = Proof_Context.pretty_name ctxt;
 
     fun prt_binding (b, atts) =
       Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
@@ -165,9 +167,9 @@
     fun prt_mixfix NoSyn = []
       | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
 
-    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
+    fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
-      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
+      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
           Pretty.brk 1 :: prt_mixfix mx);
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
@@ -204,11 +206,11 @@
       in (th', true) end
   | NONE => (th, false));
 
-fun thm_name kind th prts =
+fun thm_name ctxt kind th prts =
   let val head =
     if Thm.has_name_hint th then
-      Pretty.block [Pretty.keyword1 kind,
-        Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
+      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
+        Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"]
     else Pretty.keyword1 kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
@@ -244,7 +246,7 @@
       else
         let val (clauses, ctxt'') = fold_map obtain cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
-  end |> thm_name kind raw_th;
+  end |> thm_name ctxt kind raw_th;
 
 end;
 
diff -r 6e9c22c494c5 -r 5076725247fa src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 25 14:06:43 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 25 17:22:05 2016 +0200
@@ -62,6 +62,8 @@
   val facts_of: Proof.context -> Facts.T
   val facts_of_fact: Proof.context -> string -> Facts.T
   val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
+  val print_name: Proof.context -> string -> string
+  val pretty_name: Proof.context -> string -> Pretty.T
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
@@ -413,6 +415,9 @@
 
 (** pretty printing **)
 
+val print_name = Token.print_name o Thy_Header.get_keywords';
+val pretty_name = Pretty.str oo print_name;
+
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
@@ -1485,6 +1490,7 @@
 
 fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
   let
+    val prt_name = pretty_name ctxt;
     val prt_term = Syntax.pretty_term ctxt;
 
     fun prt_let (xi, t) = Pretty.block
@@ -1493,7 +1499,7 @@
 
     fun prt_asm (a, ts) =
       Pretty.block (Pretty.breaks
-        ((if a = "" then [] else [Pretty.str a, Pretty.str ":"]) @
+        ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @
           map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
@@ -1502,13 +1508,13 @@
             flat (separate sep (map (single o prt) xs))))];
   in
     Pretty.block (Pretty.fbreaks
-      (Pretty.str (name ^ ":") ::
-        prt_sect (Pretty.keyword1 "fix") [] (Pretty.str o Binding.name_of o fst) fixes @
+      (prt_name name :: Pretty.str ":" ::
+        prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
         prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
           (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
         (if forall (null o #2) asms then []
           else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
-        prt_sect (Pretty.str "subcases:") [] (Pretty.str o fst) cs))
+        prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
   end;
 
 in