author | wenzelm |
Thu, 13 Nov 2014 23:45:15 +0100 | |
changeset 58999 | ed09ae4ea2d8 |
parent 58991 | 92b6f4e68c5a |
child 59064 | a8bcb5a446c8 |
permissions | -rw-r--r-- |
58889 | 1 |
section {* Some examples with text cartouches *} |
55033 | 2 |
|
3 |
theory Cartouche_Examples |
|
4 |
imports Main |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
5 |
keywords |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
6 |
"cartouche" "term_cartouche" :: diag and |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
7 |
"text_cartouche" :: thy_decl |
55033 | 8 |
begin |
9 |
||
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
10 |
subsection {* Regular outer syntax *} |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
11 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
12 |
text \<open>Text cartouches may be used in the outer syntax category "text", |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
13 |
as alternative to the traditional "verbatim" tokens. An example is |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
14 |
this text block.\<close> -- \<open>The same works for small side-comments.\<close> |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
15 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
16 |
notepad |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
17 |
begin |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
18 |
txt \<open>Moreover, cartouches work as additional syntax in the |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
19 |
"altstring" category, for literal fact references. For example:\<close> |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
20 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
21 |
fix x y :: 'a |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
22 |
assume "x = y" |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
23 |
note \<open>x = y\<close> |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
24 |
have "x = y" by (rule \<open>x = y\<close>) |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
25 |
from \<open>x = y\<close> have "x = y" . |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
26 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
27 |
txt \<open>Of course, this can be nested inside formal comments and |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
28 |
antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
29 |
[OF \<open>x = y\<close>]}.\<close> |
56500
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56499
diff
changeset
|
30 |
|
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56499
diff
changeset
|
31 |
have "x = y" |
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56499
diff
changeset
|
32 |
by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>) -- \<open>more cartouches involving ML\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
33 |
end |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
34 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
35 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
36 |
subsection {* Outer syntax: cartouche within command syntax *} |
55033 | 37 |
|
38 |
ML {* |
|
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58889
diff
changeset
|
39 |
Outer_Syntax.command @{command_spec "cartouche"} "" |
55033 | 40 |
(Parse.cartouche >> (fn s => |
41 |
Toplevel.imperative (fn () => writeln s))) |
|
42 |
*} |
|
43 |
||
44 |
cartouche \<open>abc\<close> |
|
45 |
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close> |
|
46 |
||
47 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
48 |
subsection {* Inner syntax: string literals via cartouche *} |
55033 | 49 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
50 |
ML {* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
51 |
local |
55033 | 52 |
val mk_nib = |
53 |
Syntax.const o Lexicon.mark_const o |
|
54 |
fst o Term.dest_Const o HOLogic.mk_nibble; |
|
55 |
||
56 |
fun mk_char (s, pos) = |
|
57 |
let |
|
58 |
val c = |
|
59 |
if Symbol.is_ascii s then ord s |
|
55036 | 60 |
else if s = "\<newline>" then 10 |
55033 | 61 |
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); |
62 |
in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end; |
|
63 |
||
64 |
fun mk_string [] = Const (@{const_syntax Nil}, @{typ string}) |
|
65 |
| mk_string (s :: ss) = |
|
66 |
Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; |
|
67 |
||
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
68 |
in |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
69 |
fun string_tr content args = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
70 |
let fun err () = raise TERM ("string_tr", args) in |
55033 | 71 |
(case args of |
72 |
[(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => |
|
73 |
(case Term_Position.decode_position p of |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
74 |
SOME (pos, _) => c $ mk_string (content (s, pos)) $ p |
55033 | 75 |
| NONE => err ()) |
76 |
| _ => err ()) |
|
77 |
end; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
78 |
end; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
79 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
80 |
|
55133 | 81 |
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
82 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
83 |
parse_translation {* |
55133 | 84 |
[(@{syntax_const "_cartouche_string"}, |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
85 |
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] |
55033 | 86 |
*} |
87 |
||
55133 | 88 |
term "\<open>\<close>" |
89 |
term "\<open>abc\<close>" |
|
90 |
term "\<open>abc\<close> @ \<open>xyz\<close>" |
|
91 |
term "\<open>\<newline>\<close>" |
|
92 |
term "\<open>\001\010\100\<close>" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
93 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
94 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
95 |
subsection {* Alternate outer and inner syntax: string literals *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
96 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
97 |
subsubsection {* Nested quotes *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
98 |
|
55133 | 99 |
syntax "_string_string" :: "string_position \<Rightarrow> string" ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
100 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
101 |
parse_translation {* |
55133 | 102 |
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))] |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
103 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
104 |
|
55133 | 105 |
term "\"\"" |
106 |
term "\"abc\"" |
|
107 |
term "\"abc\" @ \"xyz\"" |
|
108 |
term "\"\<newline>\"" |
|
109 |
term "\"\001\010\100\"" |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
110 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
111 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
112 |
subsubsection {* Term cartouche and regular quotes *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
113 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
114 |
ML {* |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58889
diff
changeset
|
115 |
Outer_Syntax.command @{command_spec "term_cartouche"} "" |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
116 |
(Parse.inner_syntax Parse.cartouche >> (fn s => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
117 |
Toplevel.keep (fn state => |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
118 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
119 |
val ctxt = Toplevel.context_of state; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
120 |
val t = Syntax.read_term ctxt s; |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
121 |
in writeln (Syntax.string_of_term ctxt t) end))) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
122 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
123 |
|
55133 | 124 |
term_cartouche \<open>""\<close> |
125 |
term_cartouche \<open>"abc"\<close> |
|
126 |
term_cartouche \<open>"abc" @ "xyz"\<close> |
|
127 |
term_cartouche \<open>"\<newline>"\<close> |
|
128 |
term_cartouche \<open>"\001\010\100"\<close> |
|
55033 | 129 |
|
55047 | 130 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
131 |
subsubsection {* Further nesting: antiquotations *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
132 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
133 |
setup -- "ML antiquotation" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
134 |
{* |
56072 | 135 |
ML_Antiquotation.inline @{binding term_cartouche} |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
136 |
(Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
137 |
(fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
138 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
139 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
140 |
setup -- "document antiquotation" |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
141 |
{* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
142 |
Thy_Output.antiquotation @{binding ML_cartouche} |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
143 |
(Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source => |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
144 |
let |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
145 |
val toks = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
146 |
ML_Lex.read Position.none "fn _ => (" @ |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56275
diff
changeset
|
147 |
ML_Lex.read_source false source @ |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
148 |
ML_Lex.read Position.none ");"; |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58928
diff
changeset
|
149 |
val (pos, _) = #range source; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58928
diff
changeset
|
150 |
val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks; |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
151 |
in "" end); |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
152 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
153 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
154 |
ML {* |
55133 | 155 |
@{term_cartouche \<open>""\<close>}; |
156 |
@{term_cartouche \<open>"abc"\<close>}; |
|
157 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
158 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
159 |
@{term_cartouche \<open>"\001\010\100"\<close>}; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
160 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
161 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
162 |
text {* |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
163 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
164 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
165 |
( |
55133 | 166 |
@{term_cartouche \<open>""\<close>}; |
167 |
@{term_cartouche \<open>"abc"\<close>}; |
|
168 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
169 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
170 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
171 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
172 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
173 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
174 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
175 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
176 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
177 |
subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
178 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
179 |
ML {* |
55110
917e799f19da
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
wenzelm
parents:
55109
diff
changeset
|
180 |
Outer_Syntax.command |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
181 |
@{command_spec "text_cartouche"} "" |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58991
diff
changeset
|
182 |
(Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command) |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
183 |
*} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
184 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
185 |
text_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
186 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
187 |
@{ML_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
188 |
\<open> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
189 |
( |
55133 | 190 |
@{term_cartouche \<open>""\<close>}; |
191 |
@{term_cartouche \<open>"abc"\<close>}; |
|
192 |
@{term_cartouche \<open>"abc" @ "xyz"\<close>}; |
|
193 |
@{term_cartouche \<open>"\<newline>"\<close>}; |
|
194 |
@{term_cartouche \<open>"\001\010\100"\<close>} |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
195 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
196 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
197 |
} |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
198 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
199 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
200 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
201 |
subsection {* Proof method syntax: ML tactic expression *} |
55047 | 202 |
|
203 |
ML {* |
|
204 |
structure ML_Tactic: |
|
205 |
sig |
|
206 |
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
207 |
val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic |
55047 | 208 |
end = |
209 |
struct |
|
210 |
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); |
|
211 |
||
212 |
val set = Data.put; |
|
213 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
214 |
fun ml_tactic source ctxt = |
55047 | 215 |
let |
216 |
val ctxt' = ctxt |> Context.proof_map |
|
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
217 |
(ML_Context.expression (#range source) "tactic" "Proof.context -> tactic" |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
218 |
"Context.map_proof (ML_Tactic.set tactic)" |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
219 |
(ML_Lex.read Position.none "fn ctxt: Proof.context =>" @ |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
220 |
ML_Lex.read_source false source)); |
55047 | 221 |
in Data.get ctxt' ctxt end; |
222 |
end; |
|
223 |
*} |
|
224 |
||
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
225 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
226 |
subsubsection {* Explicit version: method with cartouche argument *} |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
227 |
|
55047 | 228 |
method_setup ml_tactic = {* |
229 |
Scan.lift Args.cartouche_source_position |
|
230 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
|
231 |
*} |
|
232 |
||
233 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
234 |
apply (ml_tactic \<open>rtac @{thm impI} 1\<close>) |
|
235 |
apply (ml_tactic \<open>etac @{thm conjE} 1\<close>) |
|
236 |
apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>) |
|
237 |
apply (ml_tactic \<open>ALLGOALS atac\<close>) |
|
238 |
done |
|
239 |
||
240 |
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>) |
|
241 |
||
242 |
ML {* @{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)} *} |
|
243 |
||
244 |
text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *} |
|
245 |
||
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
246 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
247 |
subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *} |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
248 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
249 |
method_setup "cartouche" = {* |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
250 |
Scan.lift Args.cartouche_source_position |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
251 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
252 |
*} |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
253 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
254 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
255 |
apply \<open>rtac @{thm impI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
256 |
apply \<open>etac @{thm conjE} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
257 |
apply \<open>rtac @{thm conjI} 1\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
258 |
apply \<open>ALLGOALS atac\<close> |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
259 |
done |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
260 |
|
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
261 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
262 |
by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+) |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
263 |
|
55033 | 264 |
end |