equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Some examples with text cartouches\<close> |
5 section \<open>Some examples with text cartouches\<close> |
6 |
6 |
7 theory Cartouche_Examples |
7 theory Cartouche_Examples |
8 imports Main |
8 imports Main |
9 keywords |
9 keywords "cartouche" :: diag |
10 "cartouche" :: diag and |
|
11 "text_cartouche" :: thy_decl |
|
12 begin |
10 begin |
13 |
11 |
14 subsection \<open>Regular outer syntax\<close> |
12 subsection \<open>Regular outer syntax\<close> |
15 |
13 |
16 text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>, |
14 text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>, |
133 \<close> |
131 \<close> |
134 |
132 |
135 |
133 |
136 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
134 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
137 |
135 |
138 ML \<open> |
136 text |
139 Outer_Syntax.command |
|
140 \<^command_keyword>\<open>text_cartouche\<close> "" |
|
141 (Parse.opt_target -- Parse.input Parse.cartouche |
|
142 >> Document_Output.document_output_markdown) |
|
143 \<close> |
|
144 |
|
145 text_cartouche |
|
146 \<open> |
137 \<open> |
147 \<^ML>\<open> |
138 \<^ML>\<open> |
148 ( |
139 ( |
149 \<^term>\<open>""\<close>; |
140 \<^term>\<open>""\<close>; |
150 \<^term>\<open>"abc"\<close>; |
141 \<^term>\<open>"abc"\<close>; |