1 (* Title: Pure/Isar/term_style.ML |
1 (* Title: Pure/Isar/term_style.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 |
4 |
5 Styles for terms, to use with the "term_style" and "thm_style" antiquotations |
5 Styles for terms, to use with the "term_style" and "thm_style" antiquotations. |
6 *) |
6 *) |
7 |
7 |
8 (* style data *) |
|
9 signature TERM_STYLE = |
8 signature TERM_STYLE = |
10 sig |
9 sig |
11 val lookup_style: theory -> string -> (Proof.context -> term -> term) |
10 val the_style: theory -> string -> (Proof.context -> term -> term) |
12 val update_style: string -> (Proof.context -> term -> term) -> theory -> theory |
11 val add_style: string -> (Proof.context -> term -> term) -> theory -> theory |
|
12 val print_styles: theory -> unit |
13 end; |
13 end; |
14 |
14 |
15 structure TermStyle: TERM_STYLE = |
15 structure TermStyle: TERM_STYLE = |
16 struct |
16 struct |
17 |
17 |
|
18 (* style data *) |
|
19 |
|
20 fun err_dup_styles names = |
|
21 error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); |
|
22 |
18 structure StyleArgs = |
23 structure StyleArgs = |
19 struct |
24 struct |
20 val name = "Isar/style"; |
25 val name = "Isar/style"; |
21 type T = (Proof.context -> term -> term) Symtab.table; |
26 type T = ((Proof.context -> term -> term) * stamp) Symtab.table; |
22 val empty = Symtab.empty; |
27 val empty = Symtab.empty; |
23 val copy = I; |
28 val copy = I; |
24 val prep_ext = I; |
29 val prep_ext = I; |
25 fun merge x = Symtab.merge (K true) x; |
30 fun merge tabs = Symtab.merge eq_snd tabs |
26 fun print _ table = |
31 handle Symtab.DUPS dups => err_dup_styles dups; |
27 Pretty.strs ("defined styles:" :: (Symtab.keys table)) |
32 fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); |
28 |> Pretty.writeln; |
|
29 end; |
33 end; |
30 |
34 |
31 structure StyleData = TheoryDataFun(StyleArgs); |
35 structure StyleData = TheoryDataFun(StyleArgs); |
|
36 val _ = Context.add_setup [StyleData.init]; |
|
37 val print_styles = StyleData.print; |
|
38 |
32 |
39 |
33 (* accessors *) |
40 (* 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 |
41 |
39 fun update_style name style thy = |
42 fun the_style thy name = |
40 thy |
43 (case Symtab.lookup (StyleData.get thy, name) of |
41 |> StyleData.put (Symtab.update ((name, style), StyleData.get thy)); |
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 |
42 |
51 |
43 (* predefined styles *) |
52 (* predefined styles *) |
|
53 |
44 fun style_binargs ctxt t = |
54 fun style_binargs ctxt t = |
45 let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in |
55 let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in |
46 case concl of (_ $ l $ r) => (l, r) |
56 case concl of (_ $ l $ r) => (l, r) |
47 | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
57 | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
48 end; |
58 end; |
49 |
59 |
50 (* initialization *) |
60 val _ = Context.add_setup |
51 val _ = Context.add_setup [StyleData.init, |
61 [add_style "lhs" (fst oo style_binargs), |
52 update_style "lhs" (fst oo style_binargs), |
62 add_style "rhs" (snd oo style_binargs), |
53 update_style "rhs" (snd oo style_binargs), |
63 add_style "conclusion" (K Logic.strip_imp_concl)]; |
54 update_style "conclusion" (K Logic.strip_imp_concl) |
|
55 ]; |
|
56 |
64 |
57 end; |
65 end; |