--- a/src/Pure/display.ML Fri Sep 25 19:28:33 2015 +0200
+++ b/src/Pure/display.ML Fri Sep 25 19:54:51 2015 +0200
@@ -23,7 +23,6 @@
val pretty_thm_global: theory -> thm -> Pretty.T
val string_of_thm: Proof.context -> thm -> string
val string_of_thm_global: theory -> thm -> string
- val pretty_full_theory: bool -> theory -> Pretty.T list
end;
structure Display: DISPLAY =
@@ -86,92 +85,6 @@
val string_of_thm = Pretty.string_of oo pretty_thm;
val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
-
-
-(** print theory **)
-
-(* pretty_full_theory *)
-
-fun pretty_full_theory verbose thy =
- let
- val ctxt = Syntax.init_pretty_global thy;
-
- fun prt_cls c = Syntax.pretty_sort ctxt [c];
- fun prt_sort S = Syntax.pretty_sort ctxt S;
- fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
- fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
- val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
- fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
- val prt_term_no_vars = prt_term o Logic.unvarify_global;
- fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
-
- fun pretty_classrel (c, []) = prt_cls c
- | pretty_classrel (c, cs) = Pretty.block
- (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
-
- fun pretty_default S = Pretty.block
- [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
-
- val tfrees = map (fn v => TFree (v, []));
- fun pretty_type syn (t, Type.LogicalType n) =
- if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
- | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
- if syn <> syn' then NONE
- else SOME (Pretty.block
- [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
- | pretty_type syn (t, Type.Nonterminal) =
- if not syn then NONE
- else SOME (prt_typ (Type (t, [])));
-
- val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
-
- fun pretty_abbrev (c, (ty, t)) = Pretty.block
- (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
-
- fun pretty_axm (a, t) =
- Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
-
- val tsig = Sign.tsig_of thy;
- val consts = Sign.consts_of thy;
- val {const_space, constants, constraints} = Consts.dest consts;
- val {classes, default, types, ...} = Type.rep_tsig tsig;
- val type_space = Type.type_space tsig;
- val (class_space, class_algebra) = classes;
- val classes = Sorts.classes_of class_algebra;
- val arities = Sorts.arities_of class_algebra;
-
- val clsses =
- Name_Space.extern_entries verbose ctxt class_space
- (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
- |> map (apfst #1);
- val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
- val arties =
- Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities)
- |> map (apfst #1);
-
- val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
- val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
- val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
- val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
-
- val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
- in
- [Pretty.strs ("names:" :: Context.display_names thy)] @
- [Pretty.big_list "classes:" (map pretty_classrel clsses),
- pretty_default default,
- Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
- Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
- Pretty.big_list "type arities:" (pretty_arities arties),
- Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
- Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
- Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
- Pretty.big_list "axioms:" (map pretty_axm axms),
- Pretty.block
- (Pretty.breaks (Pretty.str "oracles:" ::
- map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
- end;
-
end;
structure Basic_Display: BASIC_DISPLAY = Display;