# HG changeset patch
# User wenzelm
# Date 1391441634 -3600
# Node ID 55ac31bc08a48fac57bc07a361e8b295da4a911b
# Parent  35354009ca25fe447dbff9b3043c1f843a186143
more formal markup;

diff -r 35354009ca25 -r 55ac31bc08a4 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -577,7 +577,7 @@
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t);
     fun no_constr (c, T) =
-      error ("Bad constructor: " ^ Proof_Context.extern_const ctxt c ^ "::" ^
+      error ("Bad constructor: " ^ Proof_Context.markup_const ctxt c ^ "::" ^
         Syntax.string_of_typ ctxt T);
     fun type_of_constr (cT as (_, T)) =
       let
diff -r 35354009ca25 -r 55ac31bc08a4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Pure/Isar/class.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -528,7 +528,7 @@
     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
     fun pr_param ((c, _), (v, ty)) =
       Pretty.block (Pretty.breaks
-        [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
+        [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
           Pretty.str "::", Syntax.pretty_typ lthy ty]);
   in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end;
 
@@ -538,7 +538,7 @@
     val thy = Proof_Context.theory_of lthy;
     val _ = tycos |> List.app (fn tyco =>
       if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then ()
-      else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
+      else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco)));
   in lthy end;
 
 fun instantiation (tycos, vs, sort) thy =
diff -r 35354009ca25 -r 55ac31bc08a4 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Pure/Isar/overloading.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -171,7 +171,7 @@
     val overloading = get_overloading lthy;
     fun pr_operation ((c, ty), (v, _)) =
       Pretty.block (Pretty.breaks
-        [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
+        [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
           Pretty.str "::", Syntax.pretty_typ lthy ty]);
   in Pretty.command "overloading" :: map pr_operation overloading end;
 
diff -r 35354009ca25 -r 55ac31bc08a4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -42,8 +42,14 @@
   val intern_type: Proof.context -> xstring -> string
   val intern_const: Proof.context -> xstring -> string
   val extern_class: Proof.context -> string -> xstring
+  val markup_class: Proof.context -> string -> string
+  val pretty_class: Proof.context -> string -> Pretty.T
   val extern_type: Proof.context -> string -> xstring
+  val markup_type: Proof.context -> string -> string
+  val pretty_type: Proof.context -> string -> Pretty.T
   val extern_const: Proof.context -> string -> xstring
+  val markup_const: Proof.context -> string -> string
+  val pretty_const: Proof.context -> string -> Pretty.T
   val transfer_syntax: theory -> Proof.context -> Proof.context
   val transfer: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
@@ -293,6 +299,14 @@
 fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
 fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
 
+fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
+fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
+fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup;
+
+fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str;
+fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str;
+fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str;
+
 
 (* theory transfer *)
 
diff -r 35354009ca25 -r 55ac31bc08a4 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -209,7 +209,7 @@
        | SOME const' => (const, const')) consts consts'
     val tycos_map = map2 (fn tyco =>
       fn NONE =>
-          error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
+          error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
             "\nhas a user-defined serialization")
         | SOME tyco' => (tyco, tyco')) tycos tycos';
   in (ml_code, (tycos_map, consts_map)) end;
diff -r 35354009ca25 -r 55ac31bc08a4 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Tools/Code/code_symbol.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -125,13 +125,18 @@
 fun is_value (Constant "") = true
   | is_value _ = false;
 
-fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
-  | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
-  | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
+fun quote ctxt (Constant c) =
+      Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
+  | quote ctxt (Type_Constructor tyco) =
+      "type " ^ Library.quote (Proof_Context.markup_type ctxt tyco)
+  | quote ctxt (Type_Class class) =
+      "class " ^ Library.quote (Proof_Context.markup_class ctxt class)
   | quote ctxt (Class_Relation (sub, super)) =
-      Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super)
+      Library.quote (Proof_Context.markup_class ctxt sub) ^ " < " ^
+      Library.quote (Proof_Context.markup_class ctxt super)
   | quote ctxt (Class_Instance (tyco, class)) =
-      Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class);
+      Library.quote (Proof_Context.markup_type ctxt tyco) ^ " :: " ^
+      Library.quote (Proof_Context.markup_class ctxt class);
 
 fun marker (Constant c) = "CONST " ^ c
   | marker (Type_Constructor tyco) = "TYPE " ^ tyco
diff -r 35354009ca25 -r 55ac31bc08a4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -335,7 +335,7 @@
     val _ =
       if null unimplemented then ()
       else error ("No code equations for " ^
-        commas (map (Proof_Context.extern_const ctxt) unimplemented));
+        commas (map (Proof_Context.markup_const ctxt) unimplemented));
     val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
   in (syms4, program4) end;
 
diff -r 35354009ca25 -r 55ac31bc08a4 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Tools/subtyping.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -697,7 +697,9 @@
                 (*immediate error - cannot fix complex coercion with the global algorithm*)
                 NONE =>
                   eval_error (err ++>
-                    ("No coercion known for type constructors: " ^ quote a ^ " and " ^ quote b))
+                    ("No coercion known for type constructors: " ^
+                      quote (Proof_Context.markup_type ctxt a) ^ " and " ^
+                      quote (Proof_Context.markup_type ctxt b)))
               | SOME (co, ((Ts', Us'), _)) =>
                   let
                     val co_before = gen (T1, Type (a, Ts'));
@@ -726,7 +728,9 @@
                     then mk_identity T1
                     else
                       raise COERCION_GEN_ERROR
-                        (err ++> ("No map function for " ^ quote a ^ " known"))
+                        (err ++>
+                          ("No map function for " ^ quote (Proof_Context.markup_type ctxt a)
+                            ^ " known"))
                 | SOME (tmap, variances) =>
                     let
                       val (used_coes, invarTs) =
@@ -757,7 +761,10 @@
   (case Type_Infer.deref tye T of
     Type (C, Ts) =>
       (case Symreltab.lookup (coes_of ctxt) (C, "fun") of
-        NONE => eval_error (err ++> ("No complex coercion from " ^ quote C ^ " to fun"))
+        NONE =>
+          eval_error (err ++> ("No complex coercion from " ^
+            quote (Proof_Context.markup_type ctxt C) ^ " to " ^
+            quote (Proof_Context.markup_type ctxt "fun")))
       | SOME (co, ((Ts', _), _)) =>
         let
           val co_before = gen_coercion ctxt err tye (Type (C, Ts), Type (C, Ts'));
@@ -774,7 +781,8 @@
       eval_error (err ++>
         (Pretty.string_of o Pretty.block)
          [Pretty.str "No complex coercion from", Pretty.brk 1,
-          Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1, Pretty.str "to fun"]));
+          Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1,
+          Pretty.str "to", Pretty.brk 1, Proof_Context.pretty_type ctxt "fun"]));
 
 fun insert_coercions ctxt (tye, idx) ts =
   let