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