src/Pure/Tools/named_thms.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24117 94210ad252e3
child 26363 9d95309f8069
permissions -rw-r--r--
simplified interfaces for outer syntax;
wenzelm@24047
     1
(*  Title:      Pure/Tools/named_thms.ML
wenzelm@24047
     2
    ID:         $Id$
wenzelm@24047
     3
    Author:     Makarius
wenzelm@24047
     4
wenzelm@24047
     5
Named collections of theorems in canonical order.
wenzelm@24047
     6
*)
wenzelm@24047
     7
wenzelm@24047
     8
signature NAMED_THMS =
wenzelm@24047
     9
sig
wenzelm@24047
    10
  val get: Proof.context -> thm list
wenzelm@24047
    11
  val pretty: Proof.context -> Pretty.T
wenzelm@24047
    12
  val add: attribute
wenzelm@24047
    13
  val del: attribute
wenzelm@24047
    14
  val setup: theory -> theory
wenzelm@24047
    15
end;
wenzelm@24047
    16
wenzelm@24047
    17
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
wenzelm@24047
    18
struct
wenzelm@24047
    19
wenzelm@24047
    20
structure Data = GenericDataFun
wenzelm@24047
    21
(
wenzelm@24047
    22
  type T = thm list;
wenzelm@24047
    23
  val empty = [];
wenzelm@24047
    24
  val extend = I;
wenzelm@24047
    25
  fun merge _ = Thm.merge_thms;
wenzelm@24047
    26
);
wenzelm@24047
    27
wenzelm@24047
    28
val get = Data.get o Context.Proof;
wenzelm@24047
    29
wenzelm@24047
    30
fun pretty ctxt =
wenzelm@24047
    31
  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
wenzelm@24047
    32
wenzelm@24047
    33
val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
wenzelm@24047
    34
val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
wenzelm@24047
    35
wenzelm@24047
    36
val setup =
wenzelm@24047
    37
  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
wenzelm@24047
    38
wenzelm@24867
    39
val _ =
wenzelm@24867
    40
  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
wenzelm@24117
    41
    OuterKeyword.diag
wenzelm@24117
    42
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
wenzelm@24867
    43
      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
wenzelm@24117
    44
wenzelm@24047
    45
end;