author | wenzelm |
Tue, 22 Dec 2015 16:35:41 +0100 | |
changeset 61910 | ae36547d3a30 |
parent 61903 | d5ddd4866b7b |
child 61911 | fe2b7f4276be |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
1 |
(* Title: HOL/Eisbach/method_closure.ML |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
2 |
Author: Daniel Matichuk, NICTA/UNSW |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
3 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
4 |
Facilities for treating method syntax as a closure, with abstraction |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
over terms, facts and other methods. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
The 'method' command allows to define new proof methods by combining |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
existing ones with their usual syntax. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
9 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
11 |
signature METHOD_CLOSURE = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
12 |
sig |
61818 | 13 |
val read: Proof.context -> Token.src -> Method.text |
14 |
val read_closure: Proof.context -> Token.src -> Method.text * Token.src |
|
15 |
val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src |
|
16 |
val method_text: Method.text context_parser |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
17 |
val method_evaluate: Method.text -> Proof.context -> Method.method |
61821 | 18 |
val get_method: Proof.context -> string * Position.T -> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
19 |
(term list * (string list * string list)) * Method.text |
61821 | 20 |
val eval_method: Proof.context -> (term list * string list) * Method.text -> |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
21 |
term list -> (string * thm list) list -> (Proof.context -> Method.method) list -> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
22 |
Proof.context -> Method.method |
61910 | 23 |
val method: binding -> (binding * typ option * mixfix) list -> binding list -> |
24 |
binding list -> binding list -> Token.src -> local_theory -> string * local_theory |
|
25 |
val method_cmd: binding -> (binding * string option * mixfix) list -> binding list -> |
|
26 |
binding list -> binding list -> Token.src -> local_theory -> string * local_theory |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
27 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
29 |
structure Method_Closure: METHOD_CLOSURE = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
30 |
struct |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
31 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
(* context data *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
34 |
structure Data = Generic_Data |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
35 |
( |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
36 |
type T = ((term list * (string list * string list)) * Method.text) Symtab.table; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
37 |
val empty: T = Symtab.empty; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
38 |
val extend = I; |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
39 |
fun merge data : T = Symtab.merge (K true) data; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
40 |
); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
41 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
42 |
val get_methods = Data.get o Context.Proof; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
43 |
val map_methods = Data.map; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
44 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
45 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
46 |
structure Local_Data = Proof_Data |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
47 |
( |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
48 |
type T = |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
49 |
(Proof.context -> Method.method) Symtab.table * (*dynamic methods*) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
50 |
(term list -> Proof.context -> Method.method) (*recursive method*); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
51 |
fun init _ : T = (Symtab.empty, fn _ => fn _ => Method.fail); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
52 |
); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
53 |
|
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
54 |
fun lookup_dynamic_method ctxt full_name = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
55 |
(case Symtab.lookup (#1 (Local_Data.get ctxt)) full_name of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
56 |
SOME m => m |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
57 |
| NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
58 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
59 |
val update_dynamic_method = Local_Data.map o apfst o Symtab.update; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
60 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
61 |
val get_recursive_method = #2 o Local_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
62 |
val put_recursive_method = Local_Data.map o apsnd o K; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
63 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
64 |
|
61818 | 65 |
(* read method text *) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
66 |
|
61818 | 67 |
fun read ctxt src = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
68 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
69 |
val parser = |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
70 |
Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof) |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
71 |
>> apfst (Method.check_text ctxt); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
72 |
in |
61818 | 73 |
(case Scan.read Token.stopper parser src of |
74 |
SOME (text, range) => (Method.report (text, range); text) |
|
75 |
| NONE => |
|
76 |
error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src)))) |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
77 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
78 |
|
61818 | 79 |
fun read_closure ctxt src0 = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
80 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
81 |
val src1 = map Token.init_assignable src0; |
61818 | 82 |
val text = read ctxt src1 |> Method.map_source (Method.method_closure ctxt); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
83 |
val src2 = map Token.closure src1; |
61818 | 84 |
in (text, src2) end; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
85 |
|
61818 | 86 |
fun read_closure_input ctxt = |
87 |
Input.source_explode #> |
|
88 |
Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #> |
|
89 |
read_closure ctxt; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
90 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
91 |
|
61818 | 92 |
val method_text = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
93 |
Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
94 |
(case Token.get_value tok of |
61818 | 95 |
SOME (Token.Source src) => read ctxt src |
96 |
| _ => |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
97 |
let |
61818 | 98 |
val (text, src) = read_closure_input ctxt (Token.input_of tok); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
99 |
val _ = Token.assign (SOME (Token.Source src)) tok; |
61818 | 100 |
in text end)); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
101 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
102 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
103 |
fun parse_term_args args = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
104 |
Args.context :|-- (fn ctxt => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
105 |
let |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
106 |
val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
107 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
108 |
fun parse T = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
109 |
(if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt') |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
110 |
#> Type.constraint (Type_Infer.paramify_vars T); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
111 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
112 |
fun do_parse' T = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
113 |
Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
114 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
115 |
fun do_parse (Var (_, T)) = do_parse' T |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
116 |
| do_parse (Free (_, T)) = do_parse' T |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
117 |
| do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
119 |
fun rep [] x = Scan.succeed [] x |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
120 |
| rep (t :: ts) x = (do_parse t ::: rep ts) x; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
121 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
122 |
fun check ts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
123 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
124 |
val (ts, fs) = split_list ts; |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
125 |
val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt'; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
126 |
val _ = ListPair.app (fn (f, t) => f t) (fs, ts'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
127 |
in ts' end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
128 |
in Scan.lift (rep args) >> check end); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
129 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
130 |
fun match_term_args ctxt args ts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
131 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
132 |
val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.fastype_of; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
133 |
val tyenv = fold match_types (args ~~ ts) Vartab.empty; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
134 |
val tenv = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
135 |
fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
136 |
(map Term.dest_Var args ~~ ts) Vartab.empty; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
137 |
in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
138 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
139 |
fun check_attrib ctxt attrib = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
140 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
141 |
val name = Binding.name_of attrib; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
142 |
val pos = Binding.pos_of attrib; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
143 |
val named_thm = Named_Theorems.check ctxt (name, pos); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
144 |
val parser: Method.modifier parser = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
145 |
Args.$$$ name -- Args.colon >> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
146 |
K {init = I, attribute = Named_Theorems.add named_thm, pos = pos}; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
147 |
in (named_thm, parser) end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
148 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
149 |
|
61903
d5ddd4866b7b
tuned -- with subtle change of order of evaluation;
wenzelm
parents:
61902
diff
changeset
|
150 |
fun method_evaluate text ctxt = |
61902 | 151 |
let |
61903
d5ddd4866b7b
tuned -- with subtle change of order of evaluation;
wenzelm
parents:
61902
diff
changeset
|
152 |
val text' = |
d5ddd4866b7b
tuned -- with subtle change of order of evaluation;
wenzelm
parents:
61902
diff
changeset
|
153 |
text |> (Method.map_source o map o Token.map_facts) |
61902 | 154 |
(fn SOME name => |
155 |
(case Proof_Context.lookup_fact ctxt name of |
|
156 |
SOME (false, ths) => K ths |
|
157 |
| _ => I) |
|
158 |
| NONE => I); |
|
159 |
val ctxt' = Config.put Method.closure false ctxt; |
|
61903
d5ddd4866b7b
tuned -- with subtle change of order of evaluation;
wenzelm
parents:
61902
diff
changeset
|
160 |
in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end; |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
161 |
|
61901 | 162 |
fun method_instantiate env text = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
163 |
let |
61910 | 164 |
val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env); |
61901 | 165 |
val text' = (Method.map_source o map) (Token.transform morphism) text; |
166 |
in method_evaluate text' end; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
167 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
168 |
fun setup_local_method binding lthy = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
169 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
170 |
val full_name = Local_Theory.full_name lthy binding; |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
171 |
fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
172 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
173 |
lthy |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
174 |
|> update_dynamic_method (full_name, K Method.fail) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
175 |
|> Method.local_setup binding (Scan.succeed get_method) "(internal)" |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
176 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
177 |
|
61900 | 178 |
fun dummy_named_thm named_thm = |
179 |
Context.proof_map |
|
180 |
(Named_Theorems.clear named_thm |
|
181 |
#> Named_Theorems.add_thm named_thm Drule.free_dummy_thm); |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
182 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
183 |
fun parse_method_args method_names = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
184 |
let |
60552 | 185 |
fun bind_method (name, text) ctxt = |
186 |
let |
|
187 |
val method = method_evaluate text; |
|
188 |
val inner_update = method o update_dynamic_method (name, K (method ctxt)); |
|
189 |
in update_dynamic_method (name, inner_update) ctxt end; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
190 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
191 |
fun rep [] x = Scan.succeed [] x |
61818 | 192 |
| rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
193 |
in rep method_names >> fold bind_method end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
194 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
195 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
196 |
(* FIXME redundant!? -- base name of binding is not changed by usual morphisms*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
197 |
fun Morphism_name phi name = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
198 |
Morphism.binding phi (Binding.make (name, Position.none)) |> Binding.name_of; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
199 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
200 |
fun add_method binding ((fixes, declares, methods), text) lthy = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
201 |
lthy |> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
202 |
Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
203 |
map_methods |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
204 |
(Symtab.update (Local_Theory.full_name lthy binding, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
205 |
(((map (Morphism.term phi) fixes), |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
206 |
(map (Morphism_name phi) declares, map (Morphism_name phi) methods)), |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
207 |
(Method.map_source o map) (Token.transform phi) text)))); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
208 |
|
61821 | 209 |
fun get_method ctxt (xname, pos) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
210 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
211 |
val name = Method.check_name ctxt (xname, pos); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
212 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
213 |
(case Symtab.lookup (get_methods ctxt) name of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
214 |
SOME entry => entry |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
215 |
| NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
216 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
217 |
|
61821 | 218 |
fun eval_method ctxt0 header fixes attribs methods = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
219 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
220 |
val ((term_args, hmethods), text) = header; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
221 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
222 |
fun match fixes = (* FIXME proper context!? *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
223 |
(case Seq.pull (Unify.matchers (Context.Proof ctxt0) (term_args ~~ fixes)) of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
224 |
SOME (env, _) => env |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
225 |
| NONE => error "Couldn't match term arguments"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
226 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
227 |
fun add_thms (name, thms) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
228 |
fold (Context.proof_map o Named_Theorems.add_thm name) thms; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
229 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
230 |
val setup_ctxt = fold add_thms attribs |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
231 |
#> fold update_dynamic_method (hmethods ~~ methods) |
61901 | 232 |
#> put_recursive_method (fn xs => method_instantiate (match xs) text); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
233 |
in |
61901 | 234 |
fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
235 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
236 |
|
61898 | 237 |
|
238 |
||
239 |
(** Isar command **) |
|
240 |
||
241 |
local |
|
242 |
||
61899 | 243 |
fun gen_method add_fixes name vars uses declares methods source lthy = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
244 |
let |
61898 | 245 |
val (uses_internal, lthy1) = lthy |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
246 |
|> Proof_Context.concealed |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
247 |
|> Local_Theory.open_target |-> Proof_Context.private_scope |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
248 |
|> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
249 |
|> Config.put Method.old_section_parser true |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
250 |
|> fold setup_local_method methods |
61898 | 251 |
|> fold_map (fn b => Named_Theorems.declare b "") uses; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
252 |
|
60407 | 253 |
val (term_args, lthy2) = lthy1 |
60469 | 254 |
|> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
255 |
|
61898 | 256 |
val (named_thms, modifiers) = map (check_attrib lthy2) (declares @ uses) |> split_list; |
61910 | 257 |
val method_name = Local_Theory.full_name lthy2 name; |
258 |
val method_names = map (Local_Theory.full_name lthy2) methods; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
259 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
260 |
fun parser args eval = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
261 |
apfst (Config.put_generic Method.old_section_parser true) #> |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
262 |
(parse_term_args args -- |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
263 |
parse_method_args method_names --| |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
264 |
(Scan.depend (fn context => |
61900 | 265 |
Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) -- |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
266 |
Method.sections modifiers) >> eval); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
267 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
268 |
val lthy3 = lthy2 |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
269 |
|> fold dummy_named_thm named_thms |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
270 |
|> Method.local_setup (Binding.make (Binding.name_of name, Position.none)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
271 |
(parser term_args |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
272 |
(fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
273 |
|
61818 | 274 |
val (text, src) = read_closure lthy3 source; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
275 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
276 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
277 |
Variable.export_morphism lthy3 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
278 |
(lthy |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
279 |
|> Proof_Context.transfer (Proof_Context.theory_of lthy3) |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
280 |
|> fold Token.declare_maxidx src |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
281 |
|> Variable.declare_maxidx (Variable.maxidx_of lthy3)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
282 |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
283 |
val text' = (Method.map_source o map) (Token.transform morphism) text; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
284 |
val term_args' = map (Morphism.term morphism) term_args; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
285 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
286 |
fun real_exec ts ctxt = |
61901 | 287 |
method_instantiate (match_term_args ctxt term_args' ts) text' ctxt; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
288 |
val real_parser = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
289 |
parser term_args' (fn (fixes, decl) => fn ctxt => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
290 |
real_exec fixes (put_recursive_method real_exec (decl ctxt))); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
291 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
292 |
lthy3 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
293 |
|> Local_Theory.close_target |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
294 |
|> Proof_Context.restore_naming lthy |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
295 |
|> Method.local_setup name real_parser "(defined in Eisbach)" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
296 |
|> add_method name ((term_args', named_thms, method_names), text') |
61910 | 297 |
|> pair method_name |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
298 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
299 |
|
61898 | 300 |
in |
301 |
||
61899 | 302 |
val method = gen_method Proof_Context.add_fixes; |
303 |
val method_cmd = gen_method Proof_Context.add_fixes_cmd; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
304 |
|
61898 | 305 |
end; |
306 |
||
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
307 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
308 |
Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
309 |
(Parse.binding -- Parse.for_fixes -- |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
310 |
((Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
311 |
(Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) -- |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
312 |
(Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- |
61898 | 313 |
Parse.!!! (@{keyword "="} |-- Parse.args1 (K true)) >> |
314 |
(fn ((((name, vars), (methods, uses)), declares), src) => |
|
61910 | 315 |
#2 o method_cmd name vars uses declares methods src)); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
316 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
317 |
end; |