removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
authorwenzelm
Fri Jun 17 18:33:22 2005 +0200 (2005-06-17)
changeset 16437aa87badf7a3c
parent 16436 7eb6b6cbd166
child 16438 1093f2400411
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
removed obsolete pretty_name_space;
accomodate identification of type Sign.sg and theory;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Fri Jun 17 18:33:21 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Jun 17 18:33:22 2005 +0200
     1.3 @@ -33,17 +33,14 @@
     1.4    val pretty_thm_no_quote: thm -> Pretty.T
     1.5    val pretty_thm: thm -> Pretty.T
     1.6    val pretty_thms: thm list -> Pretty.T
     1.7 -  val pretty_thm_sg: Sign.sg -> thm -> Pretty.T
     1.8 -  val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T
     1.9 +  val pretty_thm_sg: theory -> thm -> Pretty.T
    1.10 +  val pretty_thms_sg: theory -> thm list -> Pretty.T
    1.11    val pprint_thm: thm -> pprint_args -> unit
    1.12    val pretty_ctyp: ctyp -> Pretty.T
    1.13    val pprint_ctyp: ctyp -> pprint_args -> unit
    1.14    val pretty_cterm: cterm -> Pretty.T
    1.15    val pprint_cterm: cterm -> pprint_args -> unit
    1.16 -  val pretty_theory: theory -> Pretty.T
    1.17 -  val pprint_theory: theory -> pprint_args -> unit
    1.18    val pretty_full_theory: theory -> Pretty.T list
    1.19 -  val pretty_name_space: string * NameSpace.T -> Pretty.T
    1.20    val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.21    val pretty_goals: int -> thm -> Pretty.T list
    1.22    val print_goals: int -> thm -> unit
    1.23 @@ -94,7 +91,7 @@
    1.24    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.25  
    1.26  fun gen_pretty_thm quote th =
    1.27 -  pretty_thm_aux (Sign.pp (Thm.sign_of_thm th)) quote th;
    1.28 +  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote th;
    1.29  
    1.30  val pretty_thm = gen_pretty_thm true;
    1.31  val pretty_thm_no_quote = gen_pretty_thm false;
    1.32 @@ -106,8 +103,8 @@
    1.33  fun pretty_thms [th] = pretty_thm th
    1.34    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.35  
    1.36 -val pretty_thm_sg = pretty_thm oo Thm.transfer_sg;
    1.37 -val pretty_thms_sg = pretty_thms oo (map o Thm.transfer_sg);
    1.38 +val pretty_thm_sg = pretty_thm oo Thm.transfer;
    1.39 +val pretty_thms_sg = pretty_thms oo (map o Thm.transfer);
    1.40  
    1.41  
    1.42  (* top-level commands for printing theorems *)
    1.43 @@ -128,24 +125,24 @@
    1.44  (* other printing commands *)
    1.45  
    1.46  fun pretty_ctyp cT =
    1.47 -  let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end;
    1.48 +  let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
    1.49  
    1.50  fun pprint_ctyp cT =
    1.51 -  let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
    1.52 +  let val {thy, T, ...} = rep_ctyp cT in Sign.pprint_typ thy T end;
    1.53  
    1.54  fun string_of_ctyp cT =
    1.55 -  let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
    1.56 +  let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
    1.57  
    1.58  val print_ctyp = writeln o string_of_ctyp;
    1.59  
    1.60  fun pretty_cterm ct =
    1.61 -  let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end;
    1.62 +  let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
    1.63  
    1.64  fun pprint_cterm ct =
    1.65 -  let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
    1.66 +  let val {thy, t, ...} = rep_cterm ct in Sign.pprint_term thy t end;
    1.67  
    1.68  fun string_of_cterm ct =
    1.69 -  let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
    1.70 +  let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
    1.71  
    1.72  val print_cterm = writeln o string_of_cterm;
    1.73  
    1.74 @@ -153,37 +150,19 @@
    1.75  
    1.76  (** print theory **)
    1.77  
    1.78 -val pretty_theory = Sign.pretty_sg o Theory.sign_of;
    1.79 -val pprint_theory = Sign.pprint_sg o Theory.sign_of;
    1.80 -
    1.81 -val print_syntax = Syntax.print_syntax o Theory.syn_of;
    1.82 -
    1.83 -
    1.84 -(* pretty_name_space  *)
    1.85 -
    1.86 -fun pretty_name_space (kind, space) =
    1.87 -  let
    1.88 -    fun prt_entry (name, accs) = Pretty.block
    1.89 -      (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 ::
    1.90 -        Pretty.commas (map (Pretty.quote o Pretty.str) accs));
    1.91 -  in
    1.92 -    Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
    1.93 -    |> Pretty.block
    1.94 -  end;
    1.95 +val print_syntax = Syntax.print_syntax o Sign.syn_of;
    1.96  
    1.97  
    1.98  (* pretty_full_theory *)
    1.99  
   1.100  fun pretty_full_theory thy =
   1.101    let
   1.102 -    val sg = Theory.sign_of thy;
   1.103 -
   1.104 -    fun prt_cls c = Sign.pretty_sort sg [c];
   1.105 -    fun prt_sort S = Sign.pretty_sort sg S;
   1.106 -    fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
   1.107 -    fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
   1.108 +    fun prt_cls c = Sign.pretty_sort thy [c];
   1.109 +    fun prt_sort S = Sign.pretty_sort thy S;
   1.110 +    fun prt_arity t (c, Ss) = Sign.pretty_arity thy (t, Ss, [c]);
   1.111 +    fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
   1.112      val prt_typ_no_tvars = prt_typ o Type.freeze_type;
   1.113 -    fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
   1.114 +    fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
   1.115  
   1.116      fun pretty_classrel (c, []) = prt_cls c
   1.117        | pretty_classrel (c, cs) = Pretty.block
   1.118 @@ -222,9 +201,8 @@
   1.119  
   1.120      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
   1.121  
   1.122 -
   1.123 -    val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
   1.124 -    val {self = _, tsig, consts, naming, data} = Sign.rep_sg sg;
   1.125 +    val {axioms, defs, oracles} = Theory.rep_theory thy;
   1.126 +    val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
   1.127      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
   1.128  
   1.129      val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes);
   1.130 @@ -234,8 +212,8 @@
   1.131      val axms = NameSpace.extern_table axioms;
   1.132      val oras = NameSpace.extern_table oracles;
   1.133    in
   1.134 -    [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
   1.135 -      Pretty.strs ("data:" :: Sign.data_kinds data),
   1.136 +    [Pretty.strs ("names:" :: Context.names_of thy),
   1.137 +      Pretty.strs ("data:" :: Context.theory_data thy),
   1.138        Pretty.strs ["name prefix:", NameSpace.path_of naming],
   1.139        Pretty.big_list "classes:" (map pretty_classrel clsses),
   1.140        pretty_default default,
   1.141 @@ -347,7 +325,7 @@
   1.142    end;
   1.143  
   1.144  fun pretty_goals_marker bg n th =
   1.145 -  pretty_goals_aux (Sign.pp (Thm.sign_of_thm th)) bg (true, true) n th;
   1.146 +  pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) bg (true, true) n th;
   1.147  
   1.148  val pretty_goals = pretty_goals_marker "";
   1.149  val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker "";