--- 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
--- 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 =
--- 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;
--- 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 *)
--- 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;
--- 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
--- 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;
--- 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