1.1 --- a/src/Pure/Isar/term_style.ML Fri Jan 19 22:08:14 2007 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,94 +0,0 @@
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"
1.9 -antiquotations.
1.10 -*)
1.11 -
1.12 -signature TERM_STYLE =
1.13 -sig
1.14 - val the_style: theory -> string -> (Proof.context -> term -> term)
1.15 - val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
1.16 - val print_styles: theory -> unit
1.17 -end;
1.18 -
1.19 -structure TermStyle: TERM_STYLE =
1.20 -struct
1.21 -
1.22 -(* style data *)
1.23 -
1.24 -fun err_dup_styles names =
1.25 - error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
1.26 -
1.27 -structure StyleData = TheoryDataFun
1.28 -(struct
1.29 - val name = "Isar/antiquote_style";
1.30 - type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
1.31 - val empty = Symtab.empty;
1.32 - val copy = I;
1.33 - val extend = I;
1.34 - fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
1.35 - handle Symtab.DUPS dups => err_dup_styles dups;
1.36 - fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
1.37 -end);
1.38 -
1.39 -val _ = Context.add_setup StyleData.init;
1.40 -val print_styles = StyleData.print;
1.41 -
1.42 -
1.43 -(* accessors *)
1.44 -
1.45 -fun the_style thy name =
1.46 - (case Symtab.lookup (StyleData.get thy) name of
1.47 - NONE => error ("Unknown antiquote style: " ^ quote name)
1.48 - | SOME (style, _) => style);
1.49 -
1.50 -fun add_style name style thy =
1.51 - StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
1.52 - handle Symtab.DUP _ => err_dup_styles [name];
1.53 -
1.54 -
1.55 -(* predefined styles *)
1.56 -
1.57 -fun style_binargs ctxt t =
1.58 - let
1.59 - val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
1.60 - (Logic.strip_imp_concl t)
1.61 - in
1.62 - case concl of (_ $ l $ r) => (l, r)
1.63 - | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
1.64 - end;
1.65 -
1.66 -fun style_parm_premise i ctxt t =
1.67 - let val prems = Logic.strip_imp_prems t in
1.68 - if i <= length prems then nth prems (i - 1)
1.69 - else error ("Not enough premises for prem" ^ string_of_int i ^
1.70 - " in propositon: " ^ ProofContext.string_of_term ctxt t)
1.71 - end;
1.72 -
1.73 -val _ = Context.add_setup
1.74 - (add_style "lhs" (fst oo style_binargs) #>
1.75 - add_style "rhs" (snd oo style_binargs) #>
1.76 - add_style "prem1" (style_parm_premise 1) #>
1.77 - add_style "prem2" (style_parm_premise 2) #>
1.78 - add_style "prem3" (style_parm_premise 3) #>
1.79 - add_style "prem4" (style_parm_premise 4) #>
1.80 - add_style "prem5" (style_parm_premise 5) #>
1.81 - add_style "prem6" (style_parm_premise 6) #>
1.82 - add_style "prem7" (style_parm_premise 7) #>
1.83 - add_style "prem8" (style_parm_premise 8) #>
1.84 - add_style "prem9" (style_parm_premise 9) #>
1.85 - add_style "prem10" (style_parm_premise 10) #>
1.86 - add_style "prem11" (style_parm_premise 11) #>
1.87 - add_style "prem12" (style_parm_premise 12) #>
1.88 - add_style "prem13" (style_parm_premise 13) #>
1.89 - add_style "prem14" (style_parm_premise 14) #>
1.90 - add_style "prem15" (style_parm_premise 15) #>
1.91 - add_style "prem16" (style_parm_premise 16) #>
1.92 - add_style "prem17" (style_parm_premise 17) #>
1.93 - add_style "prem18" (style_parm_premise 18) #>
1.94 - add_style "prem19" (style_parm_premise 19) #>
1.95 - add_style "concl" (K Logic.strip_imp_concl));
1.96 -
1.97 -end;
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/Thy/term_style.ML Fri Jan 19 22:08:15 2007 +0100
2.3 @@ -0,0 +1,94 @@
2.4 +(* Title: Pure/Thy/term_style.ML
2.5 + ID: $Id$
2.6 + Author: Florian Haftmann, TU Muenchen
2.7 +
2.8 +Styles for terms, to use with the "term_style" and "thm_style"
2.9 +antiquotations.
2.10 +*)
2.11 +
2.12 +signature TERM_STYLE =
2.13 +sig
2.14 + val the_style: theory -> string -> (Proof.context -> term -> term)
2.15 + val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
2.16 + val print_styles: theory -> unit
2.17 +end;
2.18 +
2.19 +structure TermStyle: TERM_STYLE =
2.20 +struct
2.21 +
2.22 +(* style data *)
2.23 +
2.24 +fun err_dup_styles names =
2.25 + error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
2.26 +
2.27 +structure StyleData = TheoryDataFun
2.28 +(struct
2.29 + val name = "Isar/antiquote_style";
2.30 + type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
2.31 + val empty = Symtab.empty;
2.32 + val copy = I;
2.33 + val extend = I;
2.34 + fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
2.35 + handle Symtab.DUPS dups => err_dup_styles dups;
2.36 + fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
2.37 +end);
2.38 +
2.39 +val _ = Context.add_setup StyleData.init;
2.40 +val print_styles = StyleData.print;
2.41 +
2.42 +
2.43 +(* accessors *)
2.44 +
2.45 +fun the_style thy name =
2.46 + (case Symtab.lookup (StyleData.get thy) name of
2.47 + NONE => error ("Unknown antiquote style: " ^ quote name)
2.48 + | SOME (style, _) => style);
2.49 +
2.50 +fun add_style name style thy =
2.51 + StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
2.52 + handle Symtab.DUP _ => err_dup_styles [name];
2.53 +
2.54 +
2.55 +(* predefined styles *)
2.56 +
2.57 +fun style_binargs ctxt t =
2.58 + let
2.59 + val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
2.60 + (Logic.strip_imp_concl t)
2.61 + in
2.62 + case concl of (_ $ l $ r) => (l, r)
2.63 + | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
2.64 + end;
2.65 +
2.66 +fun style_parm_premise i ctxt t =
2.67 + let val prems = Logic.strip_imp_prems t in
2.68 + if i <= length prems then nth prems (i - 1)
2.69 + else error ("Not enough premises for prem" ^ string_of_int i ^
2.70 + " in propositon: " ^ ProofContext.string_of_term ctxt t)
2.71 + end;
2.72 +
2.73 +val _ = Context.add_setup
2.74 + (add_style "lhs" (fst oo style_binargs) #>
2.75 + add_style "rhs" (snd oo style_binargs) #>
2.76 + add_style "prem1" (style_parm_premise 1) #>
2.77 + add_style "prem2" (style_parm_premise 2) #>
2.78 + add_style "prem3" (style_parm_premise 3) #>
2.79 + add_style "prem4" (style_parm_premise 4) #>
2.80 + add_style "prem5" (style_parm_premise 5) #>
2.81 + add_style "prem6" (style_parm_premise 6) #>
2.82 + add_style "prem7" (style_parm_premise 7) #>
2.83 + add_style "prem8" (style_parm_premise 8) #>
2.84 + add_style "prem9" (style_parm_premise 9) #>
2.85 + add_style "prem10" (style_parm_premise 10) #>
2.86 + add_style "prem11" (style_parm_premise 11) #>
2.87 + add_style "prem12" (style_parm_premise 12) #>
2.88 + add_style "prem13" (style_parm_premise 13) #>
2.89 + add_style "prem14" (style_parm_premise 14) #>
2.90 + add_style "prem15" (style_parm_premise 15) #>
2.91 + add_style "prem16" (style_parm_premise 16) #>
2.92 + add_style "prem17" (style_parm_premise 17) #>
2.93 + add_style "prem18" (style_parm_premise 18) #>
2.94 + add_style "prem19" (style_parm_premise 19) #>
2.95 + add_style "concl" (K Logic.strip_imp_concl));
2.96 +
2.97 +end;