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