91 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
91 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
92 printed to a separate file, e.g. to prevent ProofGeneral from choking on massive |
92 printed to a separate file, e.g. to prevent ProofGeneral from choking on massive |
93 amounts of trace output. This redirection can be achieved using the code |
93 amounts of trace output. This redirection can be achieved using the code |
94 *} |
94 *} |
95 |
95 |
96 ML{* |
96 ML{*val strip_specials = |
97 val strip_specials = |
|
98 let |
97 let |
99 fun strip ("\^A" :: _ :: cs) = strip cs |
98 fun strip ("\^A" :: _ :: cs) = strip cs |
100 | strip (c :: cs) = c :: strip cs |
99 | strip (c :: cs) = c :: strip cs |
101 | strip [] = []; |
100 | strip [] = []; |
102 in implode o strip o explode end; |
101 in implode o strip o explode end; |
103 |
102 |
104 fun redirect_tracing stream = |
103 fun redirect_tracing stream = |
105 Output.tracing_fn := (fn s => |
104 Output.tracing_fn := (fn s => |
106 (TextIO.output (stream, (strip_specials s)); |
105 (TextIO.output (stream, (strip_specials s)); |
107 TextIO.output (stream, "\n"); |
106 TextIO.output (stream, "\n"); |
108 TextIO.flushOut stream)); |
107 TextIO.flushOut stream)) *} |
109 *} |
|
110 |
108 |
111 text {* |
109 text {* |
112 |
110 |
113 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
111 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
114 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
112 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
135 |
133 |
136 Note, however, that antiquotations are statically scoped, that is the value is |
134 Note, however, that antiquotations are statically scoped, that is the value is |
137 determined at ``compile-time'', not ``run-time''. For example the function |
135 determined at ``compile-time'', not ``run-time''. For example the function |
138 *} |
136 *} |
139 |
137 |
140 ML {* |
138 ML{*fun not_current_thyname () = Context.theory_name @{theory} *} |
141 fun not_current_thyname () = Context.theory_name @{theory} |
|
142 *} |
|
143 |
139 |
144 text {* |
140 text {* |
145 |
141 |
146 does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a |
142 does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a |
147 different theory. Instead, the code above defines the constant function |
143 different theory. Instead, the code above defines the constant function |
161 |
157 |
162 While antiquotations have many applications, they were originally introduced to |
158 While antiquotations have many applications, they were originally introduced to |
163 avoid explicit bindings for theorems such as |
159 avoid explicit bindings for theorems such as |
164 *} |
160 *} |
165 |
161 |
166 ML {* |
162 ML{*val allI = thm "allI" *} |
167 val allI = thm "allI" |
|
168 *} |
|
169 |
163 |
170 text {* |
164 text {* |
171 These bindings were difficult to maintain and also could accidentally |
165 These bindings were difficult to maintain and also could accidentally |
172 be overwritten by the user. This usually broke definitional |
166 be overwritten by the user. This usually broke definitional |
173 packages. Antiquotations solve this problem, since they are ``linked'' |
167 packages. Antiquotations solve this problem, since they are ``linked'' |
259 dynamically. For example, a function that returns the implication |
253 dynamically. For example, a function that returns the implication |
260 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"} |
254 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"} |
261 as arguments can only be written as |
255 as arguments can only be written as |
262 *} |
256 *} |
263 |
257 |
264 ML {* |
258 ML{*fun make_imp P Q tau = |
265 fun make_imp P Q tau = |
|
266 let |
259 let |
267 val x = Free ("x",tau) |
260 val x = Free ("x",tau) |
268 in Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
261 in Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
269 end |
262 end *} |
270 *} |
|
271 |
263 |
272 text {* |
264 text {* |
273 |
265 |
274 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
266 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
275 @{term "tau"} into an antiquotation. For example the following does \emph{not} work: |
267 @{term "tau"} into an antiquotation. For example the following does \emph{not} work: |
276 *} |
268 *} |
277 |
269 |
278 ML {* |
270 ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *} |
279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
|
280 *} |
|
281 |
271 |
282 text {* |
272 text {* |
283 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
273 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
284 to both functions. With @{ML make_imp} we obtain the correct term involving |
274 to both functions. With @{ML make_imp} we obtain the correct term involving |
285 @{term "S"}, @{text "T"} and @{text "@{typ nat}"} |
275 @{term "S"}, @{text "T"} and @{text "@{typ nat}"} |
321 |
311 |
322 Similarly, types can be constructed manually, for example as follows: |
312 Similarly, types can be constructed manually, for example as follows: |
323 |
313 |
324 *} |
314 *} |
325 |
315 |
326 ML {* |
316 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *} |
327 fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) |
|
328 *} |
|
329 |
317 |
330 text {* |
318 text {* |
331 which can be equally written as |
319 which can be equally written as |
332 *} |
320 *} |
333 |
321 |
334 ML {* |
322 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} |
335 fun make_fun_type tau1 tau2 = tau1 --> tau2 |
|
336 *} |
|
337 |
323 |
338 text {* |
324 text {* |
339 |
325 |
340 \begin{readmore} |
326 \begin{readmore} |
341 There are many functions in @{ML_file "Pure/logic.ML"} and |
327 There are many functions in @{ML_file "Pure/logic.ML"} and |