src/Pure/Isar/term_style.ML
changeset 15918 6d6d3fabef02
child 15960 9bd6550dc004
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/term_style.ML	Tue May 03 10:33:31 2005 +0200
     1.3 @@ -0,0 +1,64 @@
     1.4 +(*  Title:      Pure/Isar/term_style.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Styles for terms, to use with the "term_style" and "thm_style" antiquotations
     1.9 +*)
    1.10 +
    1.11 +signature STYLE =
    1.12 +sig
    1.13 +  val get_style: theory -> string -> (Term.term -> Term.term)
    1.14 +  val put_style: string -> (Term.term -> Term.term) -> theory -> theory
    1.15 +end;
    1.16 +
    1.17 +structure Style: STYLE =
    1.18 +struct
    1.19 +
    1.20 +(* exception *)
    1.21 +exception STYLE of string;
    1.22 +
    1.23 +(* style data *)
    1.24 +structure StyleArgs =
    1.25 +struct
    1.26 +  val name = "Isar/style";
    1.27 +  type T = (string * (Term.term -> Term.term)) list;
    1.28 +  val empty = [];
    1.29 +  val copy = I;
    1.30 +  val prep_ext = I;
    1.31 +  fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2);
    1.32 +    (* piecewise update of a1 by a2 *)
    1.33 +  fun print _ _ = raise (STYLE "cannot print style (not implemented)");
    1.34 +end;
    1.35 +
    1.36 +structure StyleData = TheoryDataFun(StyleArgs);
    1.37 +
    1.38 +(* accessors *)
    1.39 +fun get_style thy name =
    1.40 +  case Library.assoc_string ((StyleData.get thy), name)
    1.41 +    of NONE => raise (STYLE ("no style named " ^ name))
    1.42 +     | SOME style => style
    1.43 +
    1.44 +fun put_style name style thy =
    1.45 +  StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy;
    1.46 +
    1.47 +(* predefined styles *)
    1.48 +fun style_lhs (Const ("==", _) $ t $ _) = t
    1.49 +  | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t
    1.50 +  | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t
    1.51 +  | style_lhs (_ $ t $ _) = t
    1.52 +  | style_lhs _ = error ("Binary operator expected")
    1.53 +
    1.54 +fun style_rhs (Const ("==", _) $ _ $ t) = t
    1.55 +  | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t
    1.56 +  | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t
    1.57 +  | style_rhs (_ $ _ $ t) = t
    1.58 +  | style_rhs _ = error ("Binary operator expected")
    1.59 +
    1.60 +(* initialization *)
    1.61 +val _ = Context.add_setup [StyleData.init,
    1.62 +  put_style "lhs" style_lhs,
    1.63 +  put_style "rhs" style_rhs,
    1.64 +  put_style "conclusion" Logic.strip_imp_concl
    1.65 +];
    1.66 +
    1.67 +end;