author | wenzelm |
Tue, 24 May 2016 16:24:20 +0200 | |
changeset 63140 | 0644c2e5a989 |
parent 63120 | 629a4c5e953e |
child 63679 | dc311d55ad8f |
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 |
||
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
10 |
(* Markdown errors *) |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
11 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
12 |
local |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
13 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
14 |
fun markdown_error binding = |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
15 |
Thy_Output.antiquotation binding (Scan.succeed ()) |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
16 |
(fn {source, ...} => fn _ => |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
17 |
error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ |
62800 | 18 |
Position.here (Position.no_range_position (#1 (Token.range_of source))))) |
62153
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
19 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
20 |
in |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
21 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
22 |
val _ = |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
23 |
Theory.setup |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
24 |
(markdown_error @{binding item} #> |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
25 |
markdown_error @{binding enum} #> |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
26 |
markdown_error @{binding descr}); |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
27 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
28 |
end; |
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
29 |
|
df566b87e269
more explicit errors for control symbols that are left-over after Markdown parsing;
wenzelm
parents:
62058
diff
changeset
|
30 |
|
61619 | 31 |
(* control spacing *) |
32 |
||
33 |
val _ = |
|
34 |
Theory.setup |
|
61704 | 35 |
(Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #> |
36 |
Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #> |
|
37 |
Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #> |
|
38 |
Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip"))); |
|
61619 | 39 |
|
40 |
||
41 |
(* control style *) |
|
42 |
||
43 |
local |
|
44 |
||
45 |
fun control_antiquotation name s1 s2 = |
|
46 |
Thy_Output.antiquotation name (Scan.lift Args.cartouche_input) |
|
47 |
(fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false}); |
|
48 |
||
49 |
in |
|
50 |
||
51 |
val _ = |
|
52 |
Theory.setup |
|
53 |
(control_antiquotation @{binding footnote} "\\footnote{" "}" #> |
|
54 |
control_antiquotation @{binding emph} "\\emph{" "}" #> |
|
55 |
control_antiquotation @{binding bold} "\\textbf{" "}"); |
|
56 |
||
57 |
end; |
|
58 |
||
59 |
||
60 |
(* quasi-formal text (unchecked) *) |
|
61 |
||
62 |
local |
|
63 |
||
64 |
fun text_antiquotation name = |
|
65 |
Thy_Output.antiquotation name (Scan.lift Args.text_input) |
|
66 |
(fn {context = ctxt, ...} => fn source => |
|
67 |
(Context_Position.report ctxt (Input.pos_of source) |
|
68 |
(Markup.language_text (Input.is_delimited source)); |
|
69 |
Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)])); |
|
70 |
||
71 |
in |
|
72 |
||
73 |
val _ = |
|
74 |
Theory.setup |
|
75 |
(text_antiquotation @{binding text} #> |
|
76 |
text_antiquotation @{binding cartouche}); |
|
77 |
||
78 |
end; |
|
79 |
||
80 |
||
81 |
(* theory text with tokens (unchecked) *) |
|
82 |
||
83 |
val _ = |
|
84 |
Theory.setup |
|
85 |
(Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input) |
|
86 |
(fn {context = ctxt, ...} => fn source => |
|
87 |
let |
|
88 |
val _ = |
|
89 |
Context_Position.report ctxt (Input.pos_of source) |
|
62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62153
diff
changeset
|
90 |
(Markup.language_Isar (Input.is_delimited source)); |
61619 | 91 |
|
92 |
val keywords = Thy_Header.get_keywords' ctxt; |
|
93 |
val toks = |
|
61705
546e6494049f
trim lines for @{theory_text} similarly to @{text};
wenzelm
parents:
61704
diff
changeset
|
94 |
Input.source_explode source |
546e6494049f
trim lines for @{theory_text} similarly to @{text};
wenzelm
parents:
61704
diff
changeset
|
95 |
|> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines |
546e6494049f
trim lines for @{theory_text} similarly to @{text};
wenzelm
parents:
61704
diff
changeset
|
96 |
|> Source.of_list |
61619 | 97 |
|> Token.source' true keywords |
98 |
|> Source.exhaust; |
|
99 |
val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); |
|
61748 | 100 |
val indentation = |
101 |
Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space); |
|
61619 | 102 |
in |
103 |
implode (map Latex.output_token toks) |> |
|
61748 | 104 |
(if Config.get ctxt Thy_Output.display then |
105 |
split_lines #> map (prefix indentation) #> cat_lines #> |
|
106 |
Latex.environment "isabelle" |
|
61619 | 107 |
else enclose "\\isa{" "}") |
108 |
end)); |
|
109 |
||
110 |
||
111 |
(* goal state *) |
|
112 |
||
113 |
local |
|
114 |
||
115 |
fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ()) |
|
116 |
(fn {state, context = ctxt, ...} => fn () => |
|
117 |
Thy_Output.output ctxt |
|
118 |
[Goal_Display.pretty_goal |
|
119 |
(Config.put Goal_Display.show_main_goal main ctxt) |
|
120 |
(#goal (Proof.goal (Toplevel.proof_of state)))]); |
|
121 |
||
122 |
in |
|
123 |
||
124 |
val _ = Theory.setup |
|
125 |
(goal_state @{binding goals} true #> |
|
126 |
goal_state @{binding subgoals} false); |
|
127 |
||
128 |
end; |
|
129 |
||
130 |
||
131 |
(* embedded lemma *) |
|
132 |
||
133 |
val _ = Theory.setup |
|
134 |
(Thy_Output.antiquotation @{binding lemma} |
|
135 |
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- |
|
136 |
Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) |
|
137 |
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => |
|
138 |
let |
|
139 |
val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); |
|
140 |
val _ = Context_Position.reports ctxt reports; |
|
141 |
||
142 |
(* FIXME check proof!? *) |
|
143 |
val _ = ctxt |
|
144 |
|> Proof.theorem NONE (K I) [[(prop, [])]] |
|
145 |
|> Proof.global_terminal_proof (m1, m2); |
|
146 |
in |
|
147 |
Thy_Output.output ctxt |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61748
diff
changeset
|
148 |
(Thy_Output.maybe_pretty_source |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61748
diff
changeset
|
149 |
Thy_Output.pretty_term ctxt [hd source, prop_token] [prop]) |
61619 | 150 |
end)); |
151 |
||
152 |
||
153 |
(* verbatim text *) |
|
154 |
||
155 |
val _ = |
|
156 |
Theory.setup |
|
62520 | 157 |
(Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text_input) |
158 |
(fn {context = ctxt, ...} => fn source => |
|
159 |
(Context_Position.report ctxt (Input.pos_of source) |
|
160 |
(Markup.language_verbatim (Input.is_delimited source)); |
|
161 |
Thy_Output.verbatim_text ctxt (Input.source_content source)))); |
|
61619 | 162 |
|
163 |
||
164 |
(* ML text *) |
|
165 |
||
166 |
local |
|
167 |
||
168 |
fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input) |
|
169 |
(fn {context = ctxt, ...} => fn source => |
|
170 |
(ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source); |
|
171 |
Thy_Output.verbatim_text ctxt (Input.source_content source))); |
|
172 |
||
173 |
fun ml_enclose bg en source = |
|
174 |
ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en; |
|
175 |
||
176 |
in |
|
177 |
||
178 |
val _ = Theory.setup |
|
179 |
(ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #> |
|
180 |
ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #> |
|
181 |
ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #> |
|
182 |
ml_text @{binding ML_structure} |
|
183 |
(ml_enclose "functor XXX() = struct structure XX = " " end;") #> |
|
184 |
||
185 |
ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *) |
|
186 |
(fn source => |
|
187 |
ML_Lex.read ("ML_Env.check_functor " ^ |
|
188 |
ML_Syntax.print_string (Input.source_content source))) #> |
|
189 |
||
190 |
ml_text @{binding ML_text} (K [])); |
|
191 |
||
192 |
end; |
|
193 |
||
194 |
||
195 |
(* URLs *) |
|
196 |
||
197 |
val _ = Theory.setup |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62800
diff
changeset
|
198 |
(Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded)) |
61619 | 199 |
(fn {context = ctxt, ...} => fn (name, pos) => |
200 |
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)]; |
|
201 |
enclose "\\url{" "}" name))); |
|
202 |
||
61623 | 203 |
|
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
204 |
(* doc entries *) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
205 |
|
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
206 |
val _ = Theory.setup |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
207 |
(Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name)) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
208 |
(fn {context = ctxt, ...} => fn (name, pos) => |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
209 |
(Context_Position.report ctxt pos (Markup.doc name); |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
210 |
Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name]))); |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
211 |
|
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61623
diff
changeset
|
212 |
|
61623 | 213 |
(* formal entities *) |
214 |
||
215 |
fun entity_antiquotation name check output = |
|
216 |
Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name)) |
|
217 |
(fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name)); |
|
218 |
||
219 |
val _ = |
|
220 |
Theory.setup |
|
221 |
(entity_antiquotation @{binding command} Outer_Syntax.check_command |
|
222 |
(enclose "\\isacommand{" "}" o Output.output) #> |
|
62256 | 223 |
entity_antiquotation @{binding method} Method.check_name |
224 |
(enclose "\\isa{" "}" o Output.output) #> |
|
225 |
entity_antiquotation @{binding attribute} Attrib.check_name |
|
226 |
(enclose "\\isa{" "}" o Output.output)); |
|
61623 | 227 |
|
61619 | 228 |
end; |