author | wenzelm |
Fri, 21 May 2021 12:29:29 +0200 | |
changeset 73761 | ef1a18e20ace |
parent 73758 | 736c1b239b9d |
child 73762 | 14841c6e4d5f |
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) = |
|
73761 | 17 |
Document_Output.pretty_term ctxt (style t); |
67386 | 18 |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
19 |
fun pretty_thms_style ctxt (style: style, ths) = |
73761 | 20 |
map (fn th => Document_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 |
73761 | 24 |
in Document_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; |
67386 | 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; |
|
70326 | 33 |
val (t', _) = yield_singleton (Variable.import_terms true) t ctxt; |
73761 | 34 |
in Document_Output.pretty_term ctxt t' end; |
67386 | 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'); |
|
70308 | 46 |
val ctxt' = Proof_Context.augment eq ctxt; |
67386 | 47 |
in Proof_Context.pretty_term_abbrev ctxt' eq end; |
48 |
||
49 |
fun pretty_locale ctxt (name, pos) = |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
50 |
let val thy = Proof_Context.theory_of ctxt |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
51 |
in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; |
67386 | 52 |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
53 |
fun pretty_class ctxt s = |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
54 |
Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s)); |
67386 | 55 |
|
56 |
fun pretty_type ctxt s = |
|
57 |
let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s |
|
58 |
in Pretty.str (Proof_Context.extern_type ctxt name) end; |
|
59 |
||
70839
2136e4670ad2
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
wenzelm
parents:
70326
diff
changeset
|
60 |
fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full; |
67386 | 61 |
|
68482 | 62 |
fun pretty_theory ctxt (name, pos) = |
68484 | 63 |
(Theory.check {long = true} ctxt (name, pos); Pretty.str name); |
67386 | 64 |
|
73761 | 65 |
val basic_entity = Document_Output.antiquotation_pretty_source_embedded; |
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} => |
73761 | 70 |
Document_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs)); |
67386 | 71 |
|
72 |
val _ = Theory.setup |
|
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
73 |
(basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #> |
67386 | 74 |
basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #> |
75 |
basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #> |
|
76 |
basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #> |
|
77 |
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #> |
|
78 |
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
|
79 |
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
80 |
basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #> |
67386 | 81 |
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
82 |
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #> |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
83 |
basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #> |
67386 | 84 |
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
85 |
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
|
86 |
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
|
87 |
(fn {context = ctxt, source = src, argument = arg} => |
73761 | 88 |
Document_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg))); |
67386 | 89 |
|
73755 | 90 |
in end; |
67386 | 91 |
|
92 |
||
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
93 |
(* Markdown errors *) |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
94 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
95 |
local |
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 |
fun markdown_error binding = |
67386 | 98 |
Document_Antiquotation.setup binding (Scan.succeed ()) |
67463 | 99 |
(fn {source = src, ...} => |
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
100 |
error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ |
67463 | 101 |
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
|
102 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
103 |
val _ = |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
104 |
Theory.setup |
67147 | 105 |
(markdown_error \<^binding>\<open>item\<close> #> |
106 |
markdown_error \<^binding>\<open>enum\<close> #> |
|
107 |
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
|
108 |
|
73755 | 109 |
in end; |
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
110 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
111 |
|
61619 | 112 |
(* control spacing *) |
113 |
||
114 |
val _ = |
|
115 |
Theory.setup |
|
73761 | 116 |
(Document_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ()) |
67463 | 117 |
(fn _ => fn () => Latex.string "\\noindent") #> |
73761 | 118 |
Document_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ()) |
67463 | 119 |
(fn _ => fn () => Latex.string "\\smallskip") #> |
73761 | 120 |
Document_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ()) |
67463 | 121 |
(fn _ => fn () => Latex.string "\\medskip") #> |
73761 | 122 |
Document_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ()) |
67463 | 123 |
(fn _ => fn () => Latex.string "\\bigskip")); |
61619 | 124 |
|
125 |
||
73753 | 126 |
(* nested document text *) |
61619 | 127 |
|
128 |
local |
|
129 |
||
73753 | 130 |
fun nested_antiquotation name s1 s2 = |
73761 | 131 |
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) |
73752 | 132 |
(fn ctxt => fn txt => |
73761 | 133 |
(Context_Position.reports ctxt (Document_Output.document_reports txt); |
134 |
Latex.enclose_block s1 s2 (Document_Output.output_document ctxt {markdown = false} txt))); |
|
61619 | 135 |
|
136 |
val _ = |
|
137 |
Theory.setup |
|
73753 | 138 |
(nested_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #> |
139 |
nested_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #> |
|
140 |
nested_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}"); |
|
61619 | 141 |
|
73755 | 142 |
in end; |
61619 | 143 |
|
144 |
||
73754 | 145 |
(* index entries *) |
146 |
||
147 |
local |
|
148 |
||
73758 | 149 |
val strip_symbols = [Symbol.open_, Symbol.close, "'", "\"", "`"]; |
73756 | 150 |
|
151 |
fun strip_symbol sym = |
|
152 |
if member (op =) strip_symbols sym then "" |
|
153 |
else |
|
154 |
(case Symbol.decode sym of |
|
155 |
Symbol.Char s => s |
|
156 |
| Symbol.UTF8 s => s |
|
157 |
| Symbol.Sym s => s |
|
158 |
| Symbol.Control s => s |
|
159 |
| _ => ""); |
|
160 |
||
161 |
fun strip_antiq _ (Antiquote.Text body) = map Symbol_Pos.symbol body |
|
162 |
| strip_antiq _ (Antiquote.Control {body, ...}) = map Symbol_Pos.symbol body |
|
163 |
| strip_antiq ctxt (Antiquote.Antiq antiq) = |
|
164 |
Document_Antiquotation.read_antiq ctxt antiq |> #2 |> tl |
|
165 |
|> maps (Symbol.explode o Token.content_of); |
|
166 |
||
167 |
in |
|
168 |
||
169 |
fun clean_text ctxt txt = |
|
170 |
let |
|
171 |
val pos = Input.pos_of txt; |
|
172 |
val syms = Input.source_explode txt; |
|
173 |
val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); |
|
174 |
in ants |> maps (strip_antiq ctxt) |> map strip_symbol |> implode end; |
|
175 |
||
176 |
end; |
|
177 |
||
178 |
local |
|
179 |
||
73754 | 180 |
val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")"); |
73756 | 181 |
val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like); |
73754 | 182 |
|
73761 | 183 |
fun output_text ctxt = Latex.block o Document_Output.output_document ctxt {markdown = false}; |
73754 | 184 |
|
185 |
fun index binding def = |
|
73761 | 186 |
Document_Output.antiquotation_raw binding (Scan.lift index_args) |
73754 | 187 |
(fn ctxt => fn args => |
73756 | 188 |
let |
73761 | 189 |
val _ = Context_Position.reports ctxt (maps (Document_Output.document_reports o #1) args); |
73756 | 190 |
fun make_item (txt, opt_like) = |
191 |
let |
|
192 |
val text = output_text ctxt txt; |
|
193 |
val like = |
|
194 |
(case opt_like of |
|
195 |
SOME s => s |
|
196 |
| NONE => clean_text ctxt txt); |
|
197 |
val _ = |
|
198 |
if is_none opt_like andalso Context_Position.is_visible ctxt then |
|
199 |
writeln ("(" ^ Markup.markup Markup.keyword2 "is" ^ " " ^ quote like ^ ")" ^ |
|
200 |
Position.here (Input.pos_of txt)) |
|
201 |
else (); |
|
202 |
in {text = text, like = like} end; |
|
203 |
in Latex.index_entry {items = map make_item args, def = def} end); |
|
73754 | 204 |
|
205 |
val _ = Theory.setup (index \<^binding>\<open>index_ref\<close> false #> index \<^binding>\<open>index_def\<close> true); |
|
206 |
||
73755 | 207 |
in end; |
73754 | 208 |
|
209 |
||
61619 | 210 |
(* quasi-formal text (unchecked) *) |
211 |
||
212 |
local |
|
213 |
||
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
214 |
fun report_text ctxt text = |
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
215 |
let val pos = Input.pos_of text in |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
216 |
Context_Position.reports ctxt |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
217 |
[(pos, Markup.language_text (Input.is_delimited text)), |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
218 |
(pos, Markup.raw_text)] |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
219 |
end; |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
220 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
221 |
fun prepare_text ctxt = |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
222 |
Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt; |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
223 |
|
61619 | 224 |
fun text_antiquotation name = |
73761 | 225 |
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) |
67463 | 226 |
(fn ctxt => fn text => |
227 |
let |
|
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
228 |
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
|
229 |
in |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
230 |
prepare_text ctxt text |
73761 | 231 |
|> Document_Output.output_source ctxt |
232 |
|> Document_Output.isabelle ctxt |
|
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
233 |
end); |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
234 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
235 |
val theory_text_antiquotation = |
73761 | 236 |
Document_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input) |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
237 |
(fn ctxt => fn text => |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
238 |
let |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
239 |
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
|
240 |
|
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
241 |
val _ = report_text ctxt text; |
67463 | 242 |
val _ = |
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
243 |
Input.source_explode text |
67497 | 244 |
|> 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
|
245 |
|> maps (Token.reports keywords) |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
246 |
|> 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
|
247 |
in |
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
248 |
prepare_text ctxt text |
67495 | 249 |
|> Token.explode0 keywords |
73761 | 250 |
|> maps (Document_Output.output_token ctxt) |
251 |
|> Document_Output.isabelle ctxt |
|
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67471
diff
changeset
|
252 |
end); |
61619 | 253 |
|
254 |
val _ = |
|
255 |
Theory.setup |
|
67147 | 256 |
(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
|
257 |
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
|
258 |
theory_text_antiquotation); |
61619 | 259 |
|
73755 | 260 |
in end; |
61619 | 261 |
|
262 |
||
263 |
(* goal state *) |
|
264 |
||
265 |
local |
|
266 |
||
67463 | 267 |
fun goal_state name main = |
73761 | 268 |
Document_Output.antiquotation_pretty name (Scan.succeed ()) |
67463 | 269 |
(fn ctxt => fn () => |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
270 |
Goal_Display.pretty_goal |
61619 | 271 |
(Config.put Goal_Display.show_main_goal main ctxt) |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67497
diff
changeset
|
272 |
(#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))); |
61619 | 273 |
|
274 |
val _ = Theory.setup |
|
67147 | 275 |
(goal_state \<^binding>\<open>goals\<close> true #> |
276 |
goal_state \<^binding>\<open>subgoals\<close> false); |
|
61619 | 277 |
|
73755 | 278 |
in end; |
61619 | 279 |
|
280 |
||
281 |
(* embedded lemma *) |
|
282 |
||
283 |
val _ = Theory.setup |
|
67386 | 284 |
(Document_Antiquotation.setup \<^binding>\<open>lemma\<close> |
61619 | 285 |
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- |
286 |
Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) |
|
67463 | 287 |
(fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => |
61619 | 288 |
let |
66067 | 289 |
val reports = |
290 |
(by_pos, Markup.keyword1 |> Markup.keyword_properties) :: |
|
291 |
maps Method.reports_of (m1 :: the_list m2); |
|
61619 | 292 |
val _ = Context_Position.reports ctxt reports; |
293 |
||
294 |
(* FIXME check proof!? *) |
|
295 |
val _ = ctxt |
|
296 |
|> Proof.theorem NONE (K I) [[(prop, [])]] |
|
297 |
|> Proof.global_terminal_proof (m1, m2); |
|
70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
69965
diff
changeset
|
298 |
in |
73761 | 299 |
Document_Output.pretty_source ctxt {embedded = false} |
300 |
[hd src, prop_tok] (Document_Output.pretty_term ctxt prop) |
|
70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
69965
diff
changeset
|
301 |
end)); |
61619 | 302 |
|
303 |
||
304 |
(* verbatim text *) |
|
305 |
||
67463 | 306 |
val _ = Theory.setup |
73761 | 307 |
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input) |
67463 | 308 |
(fn ctxt => fn text => |
309 |
let |
|
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
310 |
val pos = Input.pos_of text; |
67463 | 311 |
val _ = |
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
312 |
Context_Position.reports ctxt |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
313 |
[(pos, Markup.language_verbatim (Input.is_delimited text)), |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69592
diff
changeset
|
314 |
(pos, Markup.raw_text)]; |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
315 |
in #1 (Input.source_content text) end)); |
61619 | 316 |
|
317 |
||
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
318 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
319 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
320 |
val _ = Theory.setup |
73761 | 321 |
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>bash_function\<close> |
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
322 |
(Scan.lift Args.embedded_position) Isabelle_System.check_bash_function); |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
323 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71519
diff
changeset
|
324 |
|
71146 | 325 |
(* system options *) |
326 |
||
327 |
val _ = Theory.setup |
|
73761 | 328 |
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>system_option\<close> |
71146 | 329 |
(Scan.lift Args.embedded_position) |
330 |
(fn ctxt => fn (name, pos) => |
|
331 |
let val _ = Completion.check_option (Options.default ()) ctxt (name, pos); |
|
332 |
in name end)); |
|
333 |
||
334 |
||
61619 | 335 |
(* ML text *) |
336 |
||
337 |
local |
|
338 |
||
67463 | 339 |
fun ml_text name ml = |
73761 | 340 |
Document_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input) |
67463 | 341 |
(fn ctxt => fn text => |
342 |
let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text) |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
343 |
in #1 (Input.source_content text) end); |
61619 | 344 |
|
345 |
fun ml_enclose bg en source = |
|
68823 | 346 |
ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en; |
61619 | 347 |
|
348 |
val _ = Theory.setup |
|
67147 | 349 |
(ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #> |
350 |
ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #> |
|
351 |
ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #> |
|
352 |
ml_text \<^binding>\<open>ML_structure\<close> |
|
61619 | 353 |
(ml_enclose "functor XXX() = struct structure XX = " " end;") #> |
354 |
||
67147 | 355 |
ml_text \<^binding>\<open>ML_functor\<close> (* FIXME formal treatment of functor name (!?) *) |
61619 | 356 |
(fn source => |
357 |
ML_Lex.read ("ML_Env.check_functor " ^ |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68823
diff
changeset
|
358 |
ML_Syntax.print_string (#1 (Input.source_content source)))) #> |
61619 | 359 |
|
67147 | 360 |
ml_text \<^binding>\<open>ML_text\<close> (K [])); |
61619 | 361 |
|
73755 | 362 |
in end; |
61619 | 363 |
|
364 |
||
365 |
(* URLs *) |
|
366 |
||
71519
8a96a11e0cf5
escape some special chars, notably for URL#NAME form;
wenzelm
parents:
71146
diff
changeset
|
367 |
val escape_url = |
8a96a11e0cf5
escape some special chars, notably for URL#NAME form;
wenzelm
parents:
71146
diff
changeset
|
368 |
translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c); |
8a96a11e0cf5
escape some special chars, notably for URL#NAME form;
wenzelm
parents:
71146
diff
changeset
|
369 |
|
61619 | 370 |
val _ = Theory.setup |
73761 | 371 |
(Document_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_input) |
72841 | 372 |
(fn ctxt => fn source => |
373 |
let |
|
374 |
val url = Input.string_of source; |
|
375 |
val pos = Input.pos_of source; |
|
376 |
val delimited = Input.is_delimited source; |
|
377 |
val _ = |
|
378 |
Context_Position.reports ctxt |
|
72843 | 379 |
[(pos, Markup.language_url delimited), (pos, Markup.url url)]; |
71519
8a96a11e0cf5
escape some special chars, notably for URL#NAME form;
wenzelm
parents:
71146
diff
changeset
|
380 |
in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end)); |
61619 | 381 |
|
61623 | 382 |
|
383 |
(* formal entities *) |
|
384 |
||
67463 | 385 |
local |
386 |
||
387 |
fun entity_antiquotation name check bg en = |
|
73761 | 388 |
Document_Output.antiquotation_raw name (Scan.lift Args.name_position) |
67463 | 389 |
(fn ctxt => fn (name, pos) => |
390 |
let val _ = check ctxt (name, pos) |
|
391 |
in Latex.enclose_block bg en [Latex.string (Output.output name)] end); |
|
392 |
||
61623 | 393 |
val _ = |
394 |
Theory.setup |
|
67463 | 395 |
(entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "\\isacommand{" "}" #> |
396 |
entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "\\isa{" "}" #> |
|
397 |
entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "\\isa{" "}"); |
|
61623 | 398 |
|
73755 | 399 |
in end; |
67463 | 400 |
|
401 |
end; |