--- a/src/Pure/Isar/class.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Isar/class.ML Fri Sep 25 19:13:47 2015 +0200
@@ -599,7 +599,7 @@
fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
| matchings _ = I;
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
@@ -657,7 +657,7 @@
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
val algebra = Sign.classes_of thy
- |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
+ |> fold (fn tyco => Sorts.add_arities (Context.Theory thy)
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
--- a/src/Pure/Isar/proof_context.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Sep 25 19:13:47 2015 +0200
@@ -287,7 +287,7 @@
val tsig_of = #1 o #tsig o rep_data;
val set_defsort = map_tsig o apfst o Type.set_defsort;
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
-fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
+fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
val consts_of = #1 o #consts o rep_data;
val cases_of = #cases o rep_data;
@@ -349,7 +349,7 @@
map_tsig (fn tsig as (local_tsig, global_tsig) =>
let val thy_tsig = Sign.tsig_of thy in
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
- else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
+ else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
end) |>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
@@ -555,7 +555,7 @@
fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
- in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
+ in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
in
@@ -580,8 +580,9 @@
local
-fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
- (not (abbrev_mode ctxt)) (consts_of ctxt);
+fun certify_consts ctxt =
+ Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
+ (not (abbrev_mode ctxt)) (consts_of ctxt);
fun expand_binds ctxt =
let
@@ -764,7 +765,7 @@
t
|> expand_abbrevs ctxt
|> (fn t' =>
- #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+ #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
in
--- a/src/Pure/Syntax/syntax.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Sep 25 19:13:47 2015 +0200
@@ -65,7 +65,7 @@
val is_pretty_global: Proof.context -> bool
val set_pretty_global: bool -> Proof.context -> Proof.context
val init_pretty_global: theory -> Proof.context
- val init_pretty: Context.pretty -> Proof.context
+ val init_pretty: Context.generic -> Proof.context
val pretty_term_global: theory -> term -> Pretty.T
val pretty_typ_global: theory -> typ -> Pretty.T
val pretty_sort_global: theory -> sort -> Pretty.T
@@ -324,7 +324,7 @@
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
-val init_pretty = Context.pretty_context init_pretty_global;
+val init_pretty = Context.cases init_pretty_global I;
val pretty_term_global = pretty_term o init_pretty_global;
val pretty_typ_global = pretty_typ o init_pretty_global;
--- a/src/Pure/Tools/class_deps.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML Fri Sep 25 19:13:47 2015 +0200
@@ -29,7 +29,7 @@
Graph_Display.content_node (Name_Space.extern ctxt space c)
(Class.pretty_specification (Proof_Context.theory_of ctxt) c);
in
- Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
+ Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra
|> #2 |> Sorts.classes_of |> Graph.dest
|> map (fn ((c, _), ds) => ((c, node c), ds))
end;
--- a/src/Pure/axclass.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/axclass.ML Fri Sep 25 19:13:47 2015 +0200
@@ -82,25 +82,25 @@
Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
proven_arities = proven_arities, inst_params = inst_params};
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
(
type T = data;
val empty =
make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty));
val extend = I;
- fun merge pp
+ fun merge old_thys
(Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
proven_arities = proven_arities1, inst_params = inst_params1},
Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
proven_arities = proven_arities2, inst_params = inst_params2}) =
let
- val ctxt = Syntax.init_pretty pp;
+ val old_ctxt = Syntax.init_pretty_global (fst old_thys);
val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
val params' =
if null params1 then params2
else
- fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+ fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
params2 params1;
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
--- a/src/Pure/consts.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/consts.ML Fri Sep 25 19:13:47 2015 +0200
@@ -27,7 +27,7 @@
val intern: T -> xstring -> string
val intern_syntax: T -> xstring -> string
val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
- val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
+ val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
val declare: Context.generic -> binding * typ -> T -> T
@@ -155,11 +155,11 @@
(* certify *)
-fun certify pp tsig do_expand consts =
+fun certify context tsig do_expand consts =
let
fun err msg (c, T) =
raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
- Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
+ Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
val certT = Type.cert_typ tsig;
fun cert tm =
let
@@ -272,9 +272,8 @@
fun abbreviate context tsig mode (b, raw_rhs) consts =
let
- val pp = Context.pretty_generic context;
- val cert_term = certify pp tsig false consts;
- val expand_term = certify pp tsig true consts;
+ val cert_term = certify context tsig false consts;
+ val expand_term = certify context tsig true consts;
val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
--- a/src/Pure/context.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/context.ML Fri Sep 25 19:13:47 2015 +0200
@@ -31,7 +31,6 @@
type theory_id
val theory_id: theory -> theory_id
val timing: bool Unsynchronized.ref
- type pretty
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val theory_id_name: theory_id -> string
@@ -52,7 +51,7 @@
val subthy_id: theory_id * theory_id -> bool
val subthy: theory * theory -> bool
val finish_thy: theory -> theory
- val begin_thy: (theory -> pretty) -> string -> theory list -> theory
+ val begin_thy: string -> theory list -> theory
(*proof context*)
val raw_transfer: theory -> Proof.context -> Proof.context
(*certificate*)
@@ -77,11 +76,6 @@
val proof_map: (generic -> generic) -> Proof.context -> Proof.context
val theory_of: generic -> theory (*total*)
val proof_of: generic -> Proof.context (*total*)
- (*pretty printing context*)
- val pretty: Proof.context -> pretty
- val pretty_global: theory -> pretty
- val pretty_generic: generic -> pretty
- val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
(*thread data*)
val thread_data: unit -> generic option
val the_thread_data: unit -> generic
@@ -97,7 +91,7 @@
structure Theory_Data:
sig
val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
- (pretty -> Any.T * Any.T -> Any.T) -> serial
+ (theory * theory -> Any.T * Any.T -> Any.T) -> serial
val get: serial -> (Any.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
end
@@ -114,55 +108,9 @@
(*** theory context ***)
-(** theory data **)
-
-(* data kinds and access methods *)
-
-val timing = Unsynchronized.ref false;
-
(*private copy avoids potential conflict of table exceptions*)
structure Datatab = Table(type key = int val ord = int_ord);
-datatype pretty = Pretty of Any.T;
-
-local
-
-type kind =
- {pos: Position.T,
- empty: Any.T,
- extend: Any.T -> Any.T,
- merge: pretty -> Any.T * Any.T -> Any.T};
-
-val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
-
-fun invoke name f k x =
- (case Datatab.lookup (Synchronized.value kinds) k of
- SOME kind =>
- if ! timing andalso name <> "" then
- Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
- (fn () => f kind x)
- else f kind x
- | NONE => raise Fail "Invalid theory data identifier");
-
-in
-
-fun invoke_empty k = invoke "" (K o #empty) k ();
-val invoke_extend = invoke "extend" #extend;
-fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
-
-fun declare_theory_data pos empty extend merge =
- let
- val k = serial ();
- val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
- val _ = Synchronized.change kinds (Datatab.update (k, kind));
- in k end;
-
-val extend_data = Datatab.map invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
-
-end;
-
-
(** datatype theory **)
@@ -288,6 +236,51 @@
+(** theory data **)
+
+(* data kinds and access methods *)
+
+val timing = Unsynchronized.ref false;
+
+local
+
+type kind =
+ {pos: Position.T,
+ empty: Any.T,
+ extend: Any.T -> Any.T,
+ merge: theory * theory -> Any.T * Any.T -> Any.T};
+
+val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
+
+fun invoke name f k x =
+ (case Datatab.lookup (Synchronized.value kinds) k of
+ SOME kind =>
+ if ! timing andalso name <> "" then
+ Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
+ (fn () => f kind x)
+ else f kind x
+ | NONE => raise Fail "Invalid theory data identifier");
+
+in
+
+fun invoke_empty k = invoke "" (K o #empty) k ();
+val invoke_extend = invoke "extend" #extend;
+fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+
+fun declare_theory_data pos empty extend merge =
+ let
+ val k = serial ();
+ val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
+ val _ = Synchronized.change kinds (Datatab.update (k, kind));
+ in k end;
+
+val extend_data = Datatab.map invoke_extend;
+fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
+
+end;
+
+
+
(** build theories **)
(* primitives *)
@@ -325,12 +318,12 @@
local
-fun merge_thys pp (thy1, thy2) =
+fun merge_thys (thy1, thy2) =
let
val ids = merge_ids thy1 thy2;
val history = make_history "" 0;
val ancestry = make_ancestry [] [];
- val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
+ val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
in create_thy ids history ancestry data end;
fun maximal_thys thys =
@@ -338,7 +331,7 @@
in
-fun begin_thy pp name imports =
+fun begin_thy name imports =
if name = "" then error ("Bad theory name: " ^ quote name)
else
let
@@ -351,7 +344,7 @@
(case parents of
[] => error "Missing theory imports"
| [thy] => extend_thy thy
- | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
+ | thy :: thys => Library.foldl merge_thys (thy, thys));
val history = make_history name 0;
val ancestry = make_ancestry parents ancestors;
@@ -498,17 +491,6 @@
val proof_of = cases Proof_Context.init_global I;
-(* pretty printing context *)
-
-exception PRETTY of generic;
-
-val pretty_generic = Pretty o PRETTY;
-val pretty = pretty_generic o Proof;
-val pretty_global = pretty_generic o Theory;
-
-fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
-
-
(** thread data **)
@@ -551,12 +533,12 @@
(** theory data **)
-signature THEORY_DATA_PP_ARGS =
+signature THEORY_DATA'_ARGS =
sig
type T
val empty: T
val extend: T -> T
- val merge: Context.pretty -> T * T -> T
+ val merge: theory * theory -> T * T -> T
end;
signature THEORY_DATA_ARGS =
@@ -575,7 +557,7 @@
val map: (T -> T) -> theory -> theory
end;
-functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
+functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
struct
type T = Data.T;
@@ -586,7 +568,7 @@
(Position.thread_data ())
(Data Data.empty)
(fn Data x => Data (Data.extend x))
- (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
+ (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
val get = Context.Theory_Data.get kind (fn Data x => x);
val put = Context.Theory_Data.put kind Data;
@@ -595,7 +577,7 @@
end;
functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
- Theory_Data_PP
+ Theory_Data'
(
type T = Data.T;
val empty = Data.empty;
--- a/src/Pure/defs.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/defs.ML Fri Sep 25 19:13:47 2015 +0200
@@ -13,6 +13,7 @@
val item_kind_ord: item_kind * item_kind -> order
val plain_args: typ list -> bool
type context = Proof.context * (Name_Space.T * Name_Space.T) option
+ val global_context: theory -> context
val space: context -> item_kind -> Name_Space.T
val pretty_item: context -> item -> Pretty.T
val pretty_args: Proof.context -> typ list -> Pretty.T list
@@ -55,6 +56,8 @@
type context = Proof.context * (Name_Space.T * Name_Space.T) option;
+fun global_context thy : context = (Syntax.init_pretty_global thy, NONE);
+
fun space (ctxt, spaces) kind =
(case (kind, spaces) of
(Const, SOME (const_space, _)) => const_space
--- a/src/Pure/global_theory.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/global_theory.ML Fri Sep 25 19:13:47 2015 +0200
@@ -205,9 +205,9 @@
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
let
- val ctxt = Syntax.init_pretty_global thy;
+ val context as (ctxt, _) = Defs.global_context thy;
val prop = prep ctxt (b, raw_prop);
- val ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy;
+ val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
val thm = def
|> Thm.forall_intr_frees
|> Thm.forall_elim_vars 0
--- a/src/Pure/more_thm.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/more_thm.ML Fri Sep 25 19:13:47 2015 +0200
@@ -491,7 +491,7 @@
in ((axm_name, thm), thy') end;
fun add_def_global unchecked overloaded arg thy =
- add_def (Syntax.init_pretty_global thy, NONE) unchecked overloaded arg thy;
+ add_def (Defs.global_context thy) unchecked overloaded arg thy;
--- a/src/Pure/sign.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/sign.ML Fri Sep 25 19:13:47 2015 +0200
@@ -62,7 +62,7 @@
val certify_sort: theory -> sort -> sort
val certify_typ: theory -> typ -> typ
val certify_typ_mode: Type.mode -> theory -> typ -> typ
- val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
+ val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
val certify_term: theory -> term -> term * typ * int
val cert_term: theory -> term -> term
val cert_prop: theory -> term -> term
@@ -133,20 +133,20 @@
fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
(
type T = sign;
fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
- fun merge pp (sign1, sign2) =
+ fun merge old_thys (sign1, sign2) =
let
val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
val syn = Syntax.merge_syntax (syn1, syn2);
- val tsig = Type.merge_tsig pp (tsig1, tsig2);
+ val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
in make_sign (syn, tsig, consts) end;
);
@@ -257,7 +257,7 @@
(* certify wrt. type signature *)
val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
val certify_class = Type.cert_class o tsig_of;
val certify_sort = Type.cert_sort o tsig_of;
@@ -269,14 +269,14 @@
local
-fun type_check pp tm =
+fun type_check context tm =
let
fun err_appl bs t T u U =
let
val xs = map Free bs; (*we do not rename here*)
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
- val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
+ val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
@@ -306,20 +306,19 @@
in
-fun certify' prop pp do_expand consts thy tm =
+fun certify' prop context do_expand consts thy tm =
let
val _ = check_vars tm;
val tm' = Term.map_types (certify_typ thy) tm;
- val T = type_check pp tm';
+ val T = type_check context tm';
val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
- val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
+ val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
-fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy =
- #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
+fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
+fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
end;
@@ -474,10 +473,10 @@
|> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy =
- thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
+ thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
fun primitive_arity arg thy =
- thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
+ thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
(* add translation functions *)
--- a/src/Pure/sorts.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/sorts.ML Fri Sep 25 19:13:47 2015 +0200
@@ -38,15 +38,15 @@
val minimize_sort: algebra -> sort -> sort
val complete_sort: algebra -> sort -> sort
val minimal_sorts: algebra -> sort list -> sort Ord_List.T
- val add_class: Context.pretty -> class * class list -> algebra -> algebra
- val add_classrel: Context.pretty -> class * class -> algebra -> algebra
- val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
+ val add_class: Context.generic -> class * class list -> algebra -> algebra
+ val add_classrel: Context.generic -> class * class -> algebra -> algebra
+ val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
val empty_algebra: algebra
- val merge_algebra: Context.pretty -> algebra * algebra -> algebra
- val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
+ val merge_algebra: Context.generic -> algebra * algebra -> algebra
+ val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
- val class_error: Context.pretty -> class_error -> string
+ val class_error: Context.generic -> class_error -> string
exception CLASS_ERROR of class_error
val has_instance: algebra -> string -> sort -> bool
val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*)
--- a/src/Pure/theory.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/theory.ML Fri Sep 25 19:13:47 2015 +0200
@@ -64,7 +64,7 @@
fun make_thy (pos, id, axioms, defs, wrappers) =
Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
-structure Thy = Theory_Data_PP
+structure Thy = Theory_Data'
(
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
@@ -73,13 +73,13 @@
fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
make_thy (Position.none, 0, empty_axioms, defs, wrappers);
- fun merge pp (thy1, thy2) =
+ fun merge old_thys (thy1, thy2) =
let
val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = empty_axioms;
- val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2);
+ val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
@@ -164,7 +164,7 @@
| _ => error "Bad bootstrapping of theory Pure")
else
let
- val thy = Context.begin_thy Context.pretty_global name imports;
+ val thy = Context.begin_thy name imports;
val wrappers = begin_wrappers thy;
in
thy
@@ -249,7 +249,7 @@
in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
fun add_deps_global a x y thy =
- add_deps (Syntax.init_pretty_global thy, NONE) a x y thy;
+ add_deps (Defs.global_context thy) a x y thy;
fun specify_const decl thy =
let val (t, thy') = Sign.declare_const_global decl thy;
--- a/src/Pure/type.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/type.ML Fri Sep 25 19:13:47 2015 +0200
@@ -55,7 +55,7 @@
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
val arity_number: tsig -> string -> int
- val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
+ val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
val sort_of_atyp: typ -> sort
@@ -96,9 +96,9 @@
val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
val add_nonterminal: Context.generic -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
- val add_arity: Context.pretty -> arity -> tsig -> tsig
- val add_classrel: Context.pretty -> class * class -> tsig -> tsig
- val merge_tsig: Context.pretty -> tsig * tsig -> tsig
+ val add_arity: Context.generic -> arity -> tsig -> tsig
+ val add_classrel: Context.generic -> class * class -> tsig -> tsig
+ val merge_tsig: Context.generic -> tsig * tsig -> tsig
end;
structure Type: TYPE =
@@ -321,9 +321,9 @@
| _ => error (undecl_type a));
fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
- | arity_sorts pp (TSig {classes, ...}) a S =
+ | arity_sorts context (TSig {classes, ...}) a S =
Sorts.mg_domain (#2 classes) a S
- handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+ handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err);
@@ -609,7 +609,7 @@
handle TYPE (msg, _, _) => error msg;
val _ = Binding.check c;
val (c', space') = space |> Name_Space.declare context true c;
- val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
+ val classes' = classes |> Sorts.add_class context (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -618,7 +618,7 @@
(* arities *)
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val _ =
(case lookup_type tsig t of
@@ -627,18 +627,18 @@
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
+ val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S'));
in ((space, classes'), default, types) end);
(* classrel *)
-fun add_classrel pp rel tsig =
+fun add_classrel context rel tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val rel' = apply2 (cert_class tsig) rel
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_classrel pp rel';
+ val classes' = classes |> Sorts.add_classrel context rel';
in ((space, classes'), default, types) end);
@@ -701,7 +701,7 @@
(* merge type signatures *)
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig context (tsig1, tsig2) =
let
val (TSig {classes = (space1, classes1), default = default1, types = types1,
log_types = _}) = tsig1;
@@ -709,7 +709,7 @@
log_types = _}) = tsig2;
val space' = Name_Space.merge (space1, space2);
- val classes' = Sorts.merge_algebra pp (classes1, classes2);
+ val classes' = Sorts.merge_algebra context (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;
--- a/src/Tools/Code/code_preproc.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Sep 25 19:13:47 2015 +0200
@@ -517,7 +517,7 @@
|> fold (ensure_fun ctxt arities eqngr) cs
|> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
val arities' = fold (add_arity ctxt vardeps) insts arities;
- val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
+ val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
--- a/src/Tools/Code/code_thingol.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Sep 25 19:13:47 2015 +0200
@@ -412,7 +412,7 @@
fun not_wellsorted ctxt permissive some_thm deps ty sort e =
let
- val err_class = Sorts.class_error (Context.pretty ctxt) e;
+ val err_class = Sorts.class_error (Context.Proof ctxt) e;
val err_typ =
"Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
Syntax.string_of_sort ctxt sort;