src/Pure/Isar/term_style.ML
author haftmann
Sat May 14 21:31:13 2005 +0200 (2005-05-14 ago)
changeset 15960 9bd6550dc004
parent 15918 6d6d3fabef02
child 15961 24c6b96b4a2f
permissions -rw-r--r--
added Proof.context to antiquotation
     1 (*  Title:      Pure/Isar/term_style.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Styles for terms, to use with the "term_style" and "thm_style" antiquotations
     6 *)
     7 
     8 (* style data *)
     9 signature TERM_STYLE =
    10 sig
    11   val lookup_style: theory -> string -> (Proof.context -> term -> term)
    12   val update_style: string -> (Proof.context -> term -> term) -> theory -> theory
    13 end;
    14 
    15 structure TermStyle: TERM_STYLE =
    16 struct
    17 
    18 structure StyleArgs =
    19 struct
    20   val name = "Isar/style";
    21   type T = (Proof.context -> term -> term) Symtab.table;
    22   val empty = Symtab.empty;
    23   val copy = I;
    24   val prep_ext = I;
    25   val merge = Symtab.merge (K true);
    26   fun print _ table =
    27     Pretty.strs ("defined styles:" :: (Symtab.keys table))
    28     |> Pretty.writeln;
    29 end;
    30 
    31 structure StyleData = TheoryDataFun(StyleArgs);
    32 
    33 (* accessors *)
    34 fun lookup_style thy name =
    35   case Symtab.lookup ((StyleData.get thy), name)
    36     of NONE => raise (ERROR_MESSAGE ("no style named " ^ name))
    37      | SOME style => style
    38 
    39 fun update_style name style thy =
    40   thy
    41   |> StyleData.put (Symtab.update ((name, style), StyleData.get thy));
    42 
    43 (* predefined styles *)
    44 fun style_binargs ctxt t =
    45   let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
    46     case concl of (_ $ l $ r) => (l, r)
    47         | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
    48   end;
    49 
    50 (* initialization *)
    51 val _ = Context.add_setup [StyleData.init,
    52   update_style "lhs" (fst oo style_binargs),
    53   update_style "rhs" (snd oo style_binargs),
    54   update_style "conclusion" (K Logic.strip_imp_concl)
    55 ];
    56 
    57 end;