src/Pure/Isar/term_style.ML
author nipkow
Wed Jun 01 08:44:25 2005 +0200 (2005-06-01 ago)
changeset 16160 833f4160130e
parent 15990 4ef32dcbb44f
child 16165 dbe9ee8ffcdd
permissions -rw-r--r--
added premise<i>
     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 signature TERM_STYLE =
     9 sig
    10   val the_style: theory -> string -> (Proof.context -> term -> term)
    11   val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
    12   val print_styles: theory -> unit
    13 end;
    14 
    15 structure TermStyle: TERM_STYLE =
    16 struct
    17 
    18 (* style data *)
    19 
    20 fun err_dup_styles names =
    21   error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
    22 
    23 structure StyleArgs =
    24 struct
    25   val name = "Isar/style";
    26   type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
    27   val empty = Symtab.empty;
    28   val copy = I;
    29   val prep_ext = I;
    30   fun merge tabs = Symtab.merge eq_snd tabs
    31     handle Symtab.DUPS dups => err_dup_styles dups;
    32   fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
    33 end;
    34 
    35 structure StyleData = TheoryDataFun(StyleArgs);
    36 val _ = Context.add_setup [StyleData.init];
    37 val print_styles = StyleData.print;
    38 
    39 
    40 (* accessors *)
    41 
    42 fun the_style thy name =
    43   (case Symtab.lookup (StyleData.get thy, name) of
    44     NONE => error ("Unknown antiquote style: " ^ quote name)
    45   | SOME (style, _) => style);
    46 
    47 fun add_style name style thy =
    48   StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
    49     handle Symtab.DUP _ => err_dup_styles [name];
    50 
    51 
    52 (* predefined styles *)
    53 
    54 fun style_binargs ctxt t =
    55   let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
    56     case concl of (_ $ l $ r) => (l, r)
    57     | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
    58   end;
    59 
    60 fun premise i _ t =
    61   let val prems = Logic.strip_imp_prems t
    62   in if i <= length prems then List.nth(prems,i-1)
    63      else error ("Not enough premises: premise" ^ string_of_int i)
    64   end;
    65  
    66 val _ = Context.add_setup
    67  [add_style "lhs" (fst oo style_binargs),
    68   add_style "rhs" (snd oo style_binargs),
    69   add_style "premise1" (premise 1),
    70   add_style "premise2" (premise 2),
    71   add_style "premise3" (premise 3),
    72   add_style "premise4" (premise 4),
    73   add_style "premise5" (premise 5),
    74   add_style "premise6" (premise 6),
    75   add_style "premise7" (premise 7),
    76   add_style "premise8" (premise 8),
    77   add_style "premise9" (premise 9),
    78   add_style "conclusion" (K Logic.strip_imp_concl)];
    79 
    80 end;