author | wenzelm |
Fri, 17 Jun 2005 18:33:05 +0200 | |
changeset 16424 | 18a07ad8fea8 |
parent 16167 | b2e4c4058b71 |
child 16541 | d539d47cce69 |
permissions | -rw-r--r-- |
15918 | 1 |
(* Title: Pure/Isar/term_style.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
5 |
Styles for terms, to use with the "term_style" and "thm_style" antiquotations. |
15918 | 6 |
*) |
7 |
||
15960 | 8 |
signature TERM_STYLE = |
15918 | 9 |
sig |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
10 |
val the_style: theory -> string -> (Proof.context -> term -> term) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
11 |
val add_style: string -> (Proof.context -> term -> term) -> theory -> theory |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
12 |
val print_styles: theory -> unit |
15918 | 13 |
end; |
14 |
||
15960 | 15 |
structure TermStyle: TERM_STYLE = |
15918 | 16 |
struct |
17 |
||
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
18 |
(* style data *) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
19 |
|
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
20 |
fun err_dup_styles names = |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
21 |
error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
22 |
|
16424 | 23 |
structure StyleData = TheoryDataFun |
24 |
(struct |
|
15918 | 25 |
val name = "Isar/style"; |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
26 |
type T = ((Proof.context -> term -> term) * stamp) Symtab.table; |
15960 | 27 |
val empty = Symtab.empty; |
15918 | 28 |
val copy = I; |
16424 | 29 |
val extend = I; |
30 |
fun merge _ tabs = Symtab.merge eq_snd tabs |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
31 |
handle Symtab.DUPS dups => err_dup_styles dups; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
32 |
fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); |
16424 | 33 |
end); |
15918 | 34 |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
35 |
val _ = Context.add_setup [StyleData.init]; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
36 |
val print_styles = StyleData.print; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
37 |
|
15918 | 38 |
|
39 |
(* accessors *) |
|
40 |
||
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
41 |
fun the_style thy name = |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
42 |
(case Symtab.lookup (StyleData.get thy, name) of |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
43 |
NONE => error ("Unknown antiquote style: " ^ quote name) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
44 |
| SOME (style, _) => style); |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
45 |
|
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
46 |
fun add_style name style thy = |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
47 |
StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
48 |
handle Symtab.DUP _ => err_dup_styles [name]; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
49 |
|
15918 | 50 |
|
51 |
(* predefined styles *) |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
52 |
|
15960 | 53 |
fun style_binargs ctxt t = |
16424 | 54 |
let |
55 |
val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) |
|
56 |
(Logic.strip_imp_concl t) |
|
57 |
in |
|
15960 | 58 |
case concl of (_ $ l $ r) => (l, r) |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
59 |
| _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
15960 | 60 |
end; |
15918 | 61 |
|
16167 | 62 |
fun style_parm_premise i ctxt t = |
16424 | 63 |
let val prems = Logic.strip_imp_prems t in |
64 |
if i <= length prems then List.nth (prems, i - 1) |
|
65 |
else error ("Not enough premises for prem" ^ string_of_int i ^ |
|
66 |
" in propositon: " ^ ProofContext.string_of_term ctxt t) |
|
16160 | 67 |
end; |
16167 | 68 |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
69 |
val _ = Context.add_setup |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
70 |
[add_style "lhs" (fst oo style_binargs), |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
71 |
add_style "rhs" (snd oo style_binargs), |
16167 | 72 |
add_style "prem1" (style_parm_premise 1), |
73 |
add_style "prem2" (style_parm_premise 2), |
|
74 |
add_style "prem3" (style_parm_premise 3), |
|
75 |
add_style "prem4" (style_parm_premise 4), |
|
76 |
add_style "prem5" (style_parm_premise 5), |
|
77 |
add_style "prem6" (style_parm_premise 6), |
|
78 |
add_style "prem7" (style_parm_premise 7), |
|
79 |
add_style "prem8" (style_parm_premise 8), |
|
80 |
add_style "prem9" (style_parm_premise 9), |
|
16165 | 81 |
add_style "concl" (K Logic.strip_imp_concl)]; |
15918 | 82 |
|
83 |
end; |