author | wenzelm |
Thu, 21 Jun 2018 14:29:44 +0200 | |
changeset 68481 | fb6afa538b04 |
parent 67569 | 5d71b114e7a3 |
child 68482 | cb84beb84ca9 |
permissions | -rw-r--r-- |
62058 | 1 |
(* Title: Pure/Thy/document_antiquotations.ML |
61619 | 2 |
Author: Makarius |
3 |
||
4 |
Miscellaneous document antiquotations. |
|
5 |
*) |
|
6 |
||
7 |
structure Document_Antiquotations: sig end = |
|
8 |
struct |
|
9 |
||
67386 | 10 |
(* basic entities *) |
11 |
||
12 |
local |
|
13 |
||
67463 | 14 |
type style = term -> term; |
15 |
||
16 |
fun pretty_term_style ctxt (style: style, t) = |
|
67386 | 17 |
Thy_Output.pretty_term ctxt (style t); |
18 |
||
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
19 |
fun pretty_thms_style ctxt (style: style, ths) = |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
20 |
map (fn th => Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths; |
67386 | 21 |
|
67463 | 22 |
fun pretty_term_typ ctxt (style: style, t) = |
67386 | 23 |
let val t' = style t |
24 |
in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; |
|
25 |
||
67463 | 26 |
fun pretty_term_typeof ctxt (style: style, t) = |
67386 | 27 |
Syntax.pretty_typ ctxt (Term.fastype_of (style t)); |
28 |
||
29 |
fun pretty_const ctxt c = |
|
30 |
let |
|
31 |
val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) |
|
32 |
handle TYPE (msg, _, _) => error msg; |
|
33 |
val ([t'], _) = Variable.import_terms true [t] ctxt; |
|
34 |
in Thy_Output.pretty_term ctxt t' end; |
|
35 |
||
36 |
fun pretty_abbrev ctxt s = |
|
37 |
let |
|
38 |
val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; |
|
39 |
fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); |
|
40 |
val (head, args) = Term.strip_comb t; |
|
41 |
val (c, T) = Term.dest_Const head handle TERM _ => err (); |
|
42 |
val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c |
|
43 |
handle TYPE _ => err (); |
|
44 |
val t' = Term.betapplys (Envir.expand_atom T (U, u), args); |
|
45 |
val eq = Logic.mk_equals (t, t'); |
|
46 |
val ctxt' = Variable.auto_fixes eq ctxt; |
|
47 |
in Proof_Context.pretty_term_abbrev ctxt' eq end; |
|
48 |
||
49 |
fun pretty_locale ctxt (name, pos) = |
|
50 |
let |
|
51 |
val thy = Proof_Context.theory_of ctxt |
|
52 |
in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end; |
|
53 |
||
54 |
fun pretty_class ctxt = |
|
55 |
Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; |
|
56 |
||
57 |
fun pretty_type ctxt s = |
|
58 |
let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s |
|
59 |
in Pretty.str (Proof_Context.extern_type ctxt name) end; |
|
60 |
||
61 |
fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; |
|
62 |
||
63 |
fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); |
|
64 |
||
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
65 |
val basic_entity = Thy_Output.antiquotation_pretty_source; |
67386 | 66 |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
67 |
fun basic_entities name scan pretty = |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
68 |
Document_Antiquotation.setup name scan |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
69 |
(fn {context = ctxt, source = src, argument = xs} => |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
70 |
Thy_Output.pretty_items_source ctxt src (map (pretty ctxt) xs)); |
67386 | 71 |
|
72 |
in |
|
73 |
||
74 |
val _ = Theory.setup |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
75 |
(basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #> |
67386 | 76 |
basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #> |
77 |
basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #> |
|
78 |
basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #> |
|
79 |
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #> |
|
80 |
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
|
81 |
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
|
82 |
basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #> |
|
83 |
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
|
84 |
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #> |
|
68481 | 85 |
basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #> |
67386 | 86 |
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
87 |
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #> |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
88 |
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
89 |
(fn {context = ctxt, source = src, argument = arg} => |
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
90 |
Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg))); |
67386 | 91 |
|
92 |
end; |
|
93 |
||
94 |
||
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
95 |
(* Markdown errors *) |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
96 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
97 |
local |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
98 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
99 |
fun markdown_error binding = |
67386 | 100 |
Document_Antiquotation.setup binding (Scan.succeed ()) |
67463 | 101 |
(fn {source = src, ...} => |
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
102 |
error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ |
67463 | 103 |
Position.here (Position.no_range_position (#1 (Token.range_of src))))) |
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
104 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
105 |
in |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
106 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
107 |
val _ = |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
108 |
Theory.setup |
67147 | 109 |
(markdown_error \<^binding>\<open>item\<close> #> |
110 |
markdown_error \<^binding>\<open>enum\<close> #> |
|
111 |
markdown_error \<^binding>\<open>descr\<close>); |
|
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
112 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
113 |
end; |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
114 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
115 |
|
61619 | 116 |
(* control spacing *) |
117 |
||
118 |
val _ = |
|
119 |
Theory.setup |
|
67463 | 120 |
(Thy_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ()) |
121 |
(fn _ => fn () => Latex.string "\\noindent") #> |
|
122 |
Thy_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ()) |
|
123 |
(fn _ => fn () => Latex.string "\\smallskip") #> |
|
124 |
Thy_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ()) |
|
125 |
(fn _ => fn () => Latex.string "\\medskip") #> |
|
126 |
Thy_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ()) |
|
127 |
(fn _ => fn () => Latex.string "\\bigskip")); |
|
61619 | 128 |
|
129 |
||
130 |
(* control style *) |
|
131 |
||
132 |
local |
|
133 |
||
134 |
fun control_antiquotation name s1 s2 = |
|
67463 | 135 |
Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input) |
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67505
diff
changeset
|
136 |
(fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false}); |
61619 | 137 |
|
138 |
in |
|
139 |
||
140 |
val _ = |
|
141 |
Theory.setup |
|
67147 | 142 |
(control_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #> |
143 |
control_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #> |
|
144 |
control_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}"); |
|
61619 | 145 |
|
146 |
end; |
|
147 |
||
148 |
||
149 |
(* quasi-formal text (unchecked) *) |
|
150 |
||
151 |
local |
|
152 |
||
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
153 |
fun report_text ctxt text = |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
154 |
Context_Position.report ctxt (Input.pos_of text) |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
155 |
(Markup.language_text (Input.is_delimited text)); |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
156 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
157 |
fun prepare_text ctxt = |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
158 |
Input.source_content #> Document_Antiquotation.prepare_lines ctxt; |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
159 |
|
61619 | 160 |
fun text_antiquotation name = |
67463 | 161 |
Thy_Output.antiquotation_raw name (Scan.lift Args.text_input) |
162 |
(fn ctxt => fn text => |
|
163 |
let |
|
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
164 |
val _ = report_text ctxt text; |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
165 |
in |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
166 |
prepare_text ctxt text |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
167 |
|> Thy_Output.output_source ctxt |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
168 |
|> Thy_Output.isabelle ctxt |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
169 |
end); |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
170 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
171 |
val theory_text_antiquotation = |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
172 |
Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input) |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
173 |
(fn ctxt => fn text => |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
174 |
let |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
175 |
val keywords = Thy_Header.get_keywords' ctxt; |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
176 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
177 |
val _ = report_text ctxt text; |
67463 | 178 |
val _ = |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
179 |
Input.source_explode text |
67497 | 180 |
|> Token.tokenize keywords {strict = true} |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
181 |
|> maps (Token.reports keywords) |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
182 |
|> Context_Position.reports_text ctxt; |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
183 |
in |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
184 |
prepare_text ctxt text |
67495 | 185 |
|> Token.explode0 keywords |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
186 |
|> maps (Thy_Output.output_token ctxt) |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
187 |
|> Thy_Output.isabelle ctxt |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
188 |
end); |
61619 | 189 |
|
190 |
in |
|
191 |
||
192 |
val _ = |
|
193 |
Theory.setup |
|
67147 | 194 |
(text_antiquotation \<^binding>\<open>text\<close> #> |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
195 |
text_antiquotation \<^binding>\<open>cartouche\<close> #> |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
196 |
theory_text_antiquotation); |
61619 | 197 |
|
198 |
end; |
|
199 |
||
200 |
||
201 |
||
202 |
||
203 |
(* goal state *) |
|
204 |
||
205 |
local |
|
206 |
||
67463 | 207 |
fun goal_state name main = |
208 |
Thy_Output.antiquotation_pretty name (Scan.succeed ()) |
|
209 |
(fn ctxt => fn () => |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
210 |
Goal_Display.pretty_goal |
61619 | 211 |
(Config.put Goal_Display.show_main_goal main ctxt) |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
212 |
(#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))); |
61619 | 213 |
|
214 |
in |
|
215 |
||
216 |
val _ = Theory.setup |
|
67147 | 217 |
(goal_state \<^binding>\<open>goals\<close> true #> |
218 |
goal_state \<^binding>\<open>subgoals\<close> false); |
|
61619 | 219 |
|
220 |
end; |
|
221 |
||
222 |
||
223 |
(* embedded lemma *) |
|
224 |
||
225 |
val _ = Theory.setup |
|
67386 | 226 |
(Document_Antiquotation.setup \<^binding>\<open>lemma\<close> |
61619 | 227 |
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- |
228 |
Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) |
|
67463 | 229 |
(fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => |
61619 | 230 |
let |
66067 | 231 |
val reports = |
232 |
(by_pos, Markup.keyword1 |> Markup.keyword_properties) :: |
|
233 |
maps Method.reports_of (m1 :: the_list m2); |
|
61619 | 234 |
val _ = Context_Position.reports ctxt reports; |
235 |
||
236 |
(* FIXME check proof!? *) |
|
237 |
val _ = ctxt |
|
238 |
|> Proof.theorem NONE (K I) [[(prop, [])]] |
|
239 |
|> Proof.global_terminal_proof (m1, m2); |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
240 |
in Thy_Output.pretty_source ctxt [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop) end)); |
61619 | 241 |
|
242 |
||
243 |
(* verbatim text *) |
|
244 |
||
67463 | 245 |
val _ = Theory.setup |
246 |
(Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input) |
|
247 |
(fn ctxt => fn text => |
|
248 |
let |
|
249 |
val _ = |
|
250 |
Context_Position.report ctxt (Input.pos_of text) |
|
251 |
(Markup.language_verbatim (Input.is_delimited text)); |
|
252 |
in Input.source_content text end)); |
|
61619 | 253 |
|
254 |
||
255 |
(* ML text *) |
|
256 |
||
257 |
local |
|
258 |
||
67463 | 259 |
fun ml_text name ml = |
260 |
Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input) |
|
261 |
(fn ctxt => fn text => |
|
262 |
let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text) |
|
263 |
in Input.source_content text end); |
|
61619 | 264 |
|
265 |
fun ml_enclose bg en source = |
|
266 |
ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en; |
|
267 |
||
268 |
in |
|
269 |
||
270 |
val _ = Theory.setup |
|
67147 | 271 |
(ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #> |
272 |
ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #> |
|
273 |
ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #> |
|
274 |
ml_text \<^binding>\<open>ML_structure\<close> |
|
61619 | 275 |
(ml_enclose "functor XXX() = struct structure XX = " " end;") #> |
276 |
||
67147 | 277 |
ml_text \<^binding>\<open>ML_functor\<close> (* FIXME formal treatment of functor name (!?) *) |
61619 | 278 |
(fn source => |
279 |
ML_Lex.read ("ML_Env.check_functor " ^ |
|
280 |
ML_Syntax.print_string (Input.source_content source))) #> |
|
281 |
||
67147 | 282 |
ml_text \<^binding>\<open>ML_text\<close> (K [])); |
61619 | 283 |
|
284 |
end; |
|
285 |
||
286 |
||
287 |
(* URLs *) |
|
288 |
||
289 |
val _ = Theory.setup |
|
67463 | 290 |
(Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded)) |
291 |
(fn ctxt => fn (url, pos) => |
|
292 |
let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)] |
|
293 |
in Latex.enclose_block "\\url{" "}" [Latex.string url] end)); |
|
61619 | 294 |
|
61623 | 295 |
|
296 |
(* formal entities *) |
|
297 |
||
67463 | 298 |
local |
299 |
||
300 |
fun entity_antiquotation name check bg en = |
|
301 |
Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name)) |
|
302 |
(fn ctxt => fn (name, pos) => |
|
303 |
let val _ = check ctxt (name, pos) |
|
304 |
in Latex.enclose_block bg en [Latex.string (Output.output name)] end); |
|
305 |
||
306 |
in |
|
61623 | 307 |
|
308 |
val _ = |
|
309 |
Theory.setup |
|
67463 | 310 |
(entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "\\isacommand{" "}" #> |
311 |
entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "\\isa{" "}" #> |
|
312 |
entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "\\isa{" "}"); |
|
61623 | 313 |
|
61619 | 314 |
end; |
67463 | 315 |
|
316 |
end; |