author | wenzelm |
Tue, 05 Nov 2019 14:16:16 +0100 | |
changeset 71046 | b8aeeedf7e68 |
parent 69604 | d80b2df54d31 |
child 74834 | 8d7d082c1649 |
permissions | -rw-r--r-- |
59089 | 1 |
(* Title: HOL/ex/Cartouche_Examples.thy |
2 |
Author: Makarius |
|
3 |
*) |
|
4 |
||
59068 | 5 |
section \<open>Some examples with text cartouches\<close> |
55033 | 6 |
|
7 |
theory Cartouche_Examples |
|
8 |
imports Main |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
9 |
keywords |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
10 |
"cartouche" :: diag and |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
11 |
"text_cartouche" :: thy_decl |
55033 | 12 |
begin |
13 |
||
59068 | 14 |
subsection \<open>Regular outer syntax\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
15 |
|
63054 | 16 |
text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>, |
17 |
as alternative to the traditional \<open>verbatim\<close> tokens. An example is |
|
61933 | 18 |
this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
19 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
20 |
notepad |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
21 |
begin |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
22 |
txt \<open>Cartouches work as additional syntax for embedded language tokens |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
23 |
(types, terms, props) and as a replacement for the \<open>altstring\<close> category |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
24 |
(for literal fact references). For example:\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
25 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
26 |
fix x y :: 'a |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
27 |
assume \<open>x = y\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
28 |
note \<open>x = y\<close> |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
29 |
have \<open>x = y\<close> by (rule \<open>x = y\<close>) |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
30 |
from \<open>x = y\<close> have \<open>x = y\<close> . |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
31 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
32 |
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
|
33 |
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
|
34 |
[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
|
35 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
36 |
have \<open>x = y\<close> |
69597 | 37 |
by (tactic \<open>resolve_tac \<^context> @{thms \<open>x = y\<close>} 1\<close>) |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
38 |
\<comment> \<open>more cartouches involving ML\<close> |
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
39 |
end |
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
40 |
|
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56304
diff
changeset
|
41 |
|
59068 | 42 |
subsection \<open>Outer syntax: cartouche within command syntax\<close> |
55033 | 43 |
|
59068 | 44 |
ML \<open> |
69597 | 45 |
Outer_Syntax.command \<^command_keyword>\<open>cartouche\<close> "" |
55033 | 46 |
(Parse.cartouche >> (fn s => |
60189 | 47 |
Toplevel.keep (fn _ => writeln s))) |
59068 | 48 |
\<close> |
55033 | 49 |
|
50 |
cartouche \<open>abc\<close> |
|
51 |
cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close> |
|
52 |
||
53 |
||
59068 | 54 |
subsection \<open>Inner syntax: string literals via cartouche\<close> |
55033 | 55 |
|
59068 | 56 |
ML \<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
57 |
local |
55033 | 58 |
fun mk_char (s, pos) = |
59 |
let |
|
60 |
val c = |
|
61 |
if Symbol.is_ascii s then ord s |
|
55036 | 62 |
else if s = "\<newline>" then 10 |
55033 | 63 |
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); |
69597 | 64 |
in list_comb (Syntax.const \<^const_syntax>\<open>Char\<close>, String_Syntax.mk_bits_syntax 8 c) end; |
55033 | 65 |
|
69597 | 66 |
fun mk_string [] = Const (\<^const_syntax>\<open>Nil\<close>, \<^typ>\<open>string\<close>) |
55033 | 67 |
| mk_string (s :: ss) = |
69597 | 68 |
Syntax.const \<^const_syntax>\<open>Cons\<close> $ mk_char s $ mk_string ss; |
55033 | 69 |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
70 |
in |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
71 |
fun string_tr content args = |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
72 |
let fun err () = raise TERM ("string_tr", args) in |
55033 | 73 |
(case args of |
69597 | 74 |
[(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] => |
55033 | 75 |
(case Term_Position.decode_position p of |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
76 |
SOME (pos, _) => c $ mk_string (content (s, pos)) $ p |
55033 | 77 |
| NONE => err ()) |
78 |
| _ => err ()) |
|
79 |
end; |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
80 |
end; |
59068 | 81 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
82 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
83 |
syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close> ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
84 |
|
59068 | 85 |
parse_translation \<open> |
69597 | 86 |
[(\<^syntax_const>\<open>_cartouche_string\<close>, |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
87 |
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] |
59068 | 88 |
\<close> |
55033 | 89 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
90 |
term \<open>\<open>\<close>\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
91 |
term \<open>\<open>abc\<close>\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
92 |
term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
93 |
term \<open>\<open>\<newline>\<close>\<close> |
55109
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 |
|
59068 | 96 |
subsection \<open>Alternate outer and inner syntax: string literals\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
97 |
|
59068 | 98 |
subsubsection \<open>Nested quotes\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
99 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
100 |
syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close> ("_") |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
101 |
|
59068 | 102 |
parse_translation \<open> |
69597 | 103 |
[(\<^syntax_const>\<open>_string_string\<close>, K (string_tr Lexicon.explode_string))] |
59068 | 104 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
105 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
106 |
term \<open>""\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
107 |
term \<open>"abc"\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
108 |
term \<open>"abc" @ "xyz"\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
109 |
term \<open>"\<newline>"\<close> |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
110 |
term \<open>"\001\010\100"\<close> |
55033 | 111 |
|
55047 | 112 |
|
59068 | 113 |
subsubsection \<open>Further nesting: antiquotations\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
114 |
|
59068 | 115 |
ML \<open> |
69597 | 116 |
\<^term>\<open>""\<close>; |
117 |
\<^term>\<open>"abc"\<close>; |
|
118 |
\<^term>\<open>"abc" @ "xyz"\<close>; |
|
119 |
\<^term>\<open>"\<newline>"\<close>; |
|
120 |
\<^term>\<open>"\001\010\100"\<close>; |
|
59068 | 121 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
122 |
|
59068 | 123 |
text \<open> |
69597 | 124 |
\<^ML>\<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
125 |
( |
69604 | 126 |
\<^term>\<open>""\<close>; |
127 |
\<^term>\<open>"abc"\<close>; |
|
128 |
\<^term>\<open>"abc" @ "xyz"\<close>; |
|
129 |
\<^term>\<open>"\<newline>"\<close>; |
|
130 |
\<^term>\<open>"\001\010\100"\<close> |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
131 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
132 |
\<close> |
59068 | 133 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
134 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
135 |
|
59068 | 136 |
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
137 |
|
59068 | 138 |
ML \<open> |
55110
917e799f19da
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
wenzelm
parents:
55109
diff
changeset
|
139 |
Outer_Syntax.command |
69597 | 140 |
\<^command_keyword>\<open>text_cartouche\<close> "" |
61457 | 141 |
(Parse.opt_target -- Parse.input Parse.cartouche |
67382 | 142 |
>> Pure_Syn.document_command {markdown = true}) |
59068 | 143 |
\<close> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
144 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
145 |
text_cartouche |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
146 |
\<open> |
69597 | 147 |
\<^ML>\<open> |
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
148 |
( |
69604 | 149 |
\<^term>\<open>""\<close>; |
150 |
\<^term>\<open>"abc"\<close>; |
|
151 |
\<^term>\<open>"abc" @ "xyz"\<close>; |
|
152 |
\<^term>\<open>"\<newline>"\<close>; |
|
153 |
\<^term>\<open>"\001\010\100"\<close> |
|
55109
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
154 |
) |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
155 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
156 |
\<close> |
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
157 |
|
ecff9e26360c
more cartouche examples, including uniform nesting of sub-languages;
wenzelm
parents:
55048
diff
changeset
|
158 |
|
59068 | 159 |
subsection \<open>Proof method syntax: ML tactic expression\<close> |
55047 | 160 |
|
59068 | 161 |
ML \<open> |
55047 | 162 |
structure ML_Tactic: |
163 |
sig |
|
164 |
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context |
|
59064 | 165 |
val ml_tactic: Input.source -> Proof.context -> tactic |
55047 | 166 |
end = |
167 |
struct |
|
168 |
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); |
|
169 |
||
170 |
val set = Data.put; |
|
171 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55133
diff
changeset
|
172 |
fun ml_tactic source ctxt = |
55047 | 173 |
let |
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
174 |
val ctxt' = ctxt |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
175 |
|> Context.proof_map (ML_Context.expression (Input.pos_of source) |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
176 |
(ML_Lex.read "Theory.local_setup (ML_Tactic.set (fn ctxt: Proof.context => (" @ |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
177 |
ML_Lex.read_source source @ ML_Lex.read ")))")); |
55047 | 178 |
in Data.get ctxt' ctxt end; |
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
179 |
end |
59068 | 180 |
\<close> |
55047 | 181 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
182 |
|
59068 | 183 |
subsubsection \<open>Explicit version: method with cartouche argument\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
184 |
|
59068 | 185 |
method_setup ml_tactic = \<open> |
59809 | 186 |
Scan.lift Args.cartouche_input |
55047 | 187 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
59068 | 188 |
\<close> |
55047 | 189 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
190 |
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> |
69597 | 191 |
apply (ml_tactic \<open>resolve_tac \<^context> @{thms impI} 1\<close>) |
192 |
apply (ml_tactic \<open>eresolve_tac \<^context> @{thms conjE} 1\<close>) |
|
193 |
apply (ml_tactic \<open>resolve_tac \<^context> @{thms conjI} 1\<close>) |
|
194 |
apply (ml_tactic \<open>ALLGOALS (assume_tac \<^context>)\<close>) |
|
55047 | 195 |
done |
196 |
||
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
197 |
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>) |
55047 | 198 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
199 |
ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close> |
55047 | 200 |
|
69597 | 201 |
text \<open>\<^ML>\<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>\<close> |
55047 | 202 |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
203 |
|
59068 | 204 |
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
205 |
|
59068 | 206 |
method_setup "cartouche" = \<open> |
59809 | 207 |
Scan.lift Args.cartouche_input |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
208 |
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
59068 | 209 |
\<close> |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
210 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
211 |
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> |
69597 | 212 |
apply \<open>resolve_tac \<^context> @{thms impI} 1\<close> |
213 |
apply \<open>eresolve_tac \<^context> @{thms conjE} 1\<close> |
|
214 |
apply \<open>resolve_tac \<^context> @{thms conjI} 1\<close> |
|
215 |
apply \<open>ALLGOALS (assume_tac \<^context>)\<close> |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
216 |
done |
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
217 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63054
diff
changeset
|
218 |
lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> |
69597 | 219 |
by (\<open>resolve_tac \<^context> @{thms impI} 1\<close>, |
220 |
\<open>eresolve_tac \<^context> @{thms conjE} 1\<close>, |
|
221 |
\<open>resolve_tac \<^context> @{thms conjI} 1\<close>, |
|
222 |
\<open>assume_tac \<^context> 1\<close>+) |
|
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
55047
diff
changeset
|
223 |
|
59112 | 224 |
|
59128 | 225 |
subsection \<open>ML syntax\<close> |
59112 | 226 |
|
59128 | 227 |
text \<open>Input source with position information:\<close> |
59112 | 228 |
ML \<open> |
59135 | 229 |
val s: Input.source = \<open>abc123def456\<close>; |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59135
diff
changeset
|
230 |
Output.information ("Look here!" ^ Position.here (Input.pos_of s)); |
59112 | 231 |
|
232 |
\<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) => |
|
233 |
if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); |
|
234 |
\<close> |
|
235 |
||
55033 | 236 |
end |