61619
|
1 |
(* Title: Pure/ML/document_antiquotations.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Miscellaneous document antiquotations.
|
|
5 |
*)
|
|
6 |
|
|
7 |
structure Document_Antiquotations: sig end =
|
|
8 |
struct
|
|
9 |
|
|
10 |
(* control spacing *)
|
|
11 |
|
|
12 |
val _ =
|
|
13 |
Theory.setup
|
|
14 |
(Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
|
|
15 |
Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
|
|
16 |
Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
|
|
17 |
Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
|
|
18 |
|
|
19 |
|
|
20 |
(* control style *)
|
|
21 |
|
|
22 |
local
|
|
23 |
|
|
24 |
fun control_antiquotation name s1 s2 =
|
|
25 |
Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
|
|
26 |
(fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
|
|
27 |
|
|
28 |
in
|
|
29 |
|
|
30 |
val _ =
|
|
31 |
Theory.setup
|
|
32 |
(control_antiquotation @{binding footnote} "\\footnote{" "}" #>
|
|
33 |
control_antiquotation @{binding emph} "\\emph{" "}" #>
|
|
34 |
control_antiquotation @{binding bold} "\\textbf{" "}");
|
|
35 |
|
|
36 |
end;
|
|
37 |
|
|
38 |
|
|
39 |
(* quasi-formal text (unchecked) *)
|
|
40 |
|
|
41 |
local
|
|
42 |
|
|
43 |
fun text_antiquotation name =
|
|
44 |
Thy_Output.antiquotation name (Scan.lift Args.text_input)
|
|
45 |
(fn {context = ctxt, ...} => fn source =>
|
|
46 |
(Context_Position.report ctxt (Input.pos_of source)
|
|
47 |
(Markup.language_text (Input.is_delimited source));
|
|
48 |
Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
|
|
49 |
|
|
50 |
in
|
|
51 |
|
|
52 |
val _ =
|
|
53 |
Theory.setup
|
|
54 |
(text_antiquotation @{binding text} #>
|
|
55 |
text_antiquotation @{binding cartouche});
|
|
56 |
|
|
57 |
end;
|
|
58 |
|
|
59 |
|
|
60 |
(* theory text with tokens (unchecked) *)
|
|
61 |
|
|
62 |
val _ =
|
|
63 |
Theory.setup
|
|
64 |
(Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
|
|
65 |
(fn {context = ctxt, ...} => fn source =>
|
|
66 |
let
|
|
67 |
val _ =
|
|
68 |
Context_Position.report ctxt (Input.pos_of source)
|
|
69 |
(Markup.language_outer (Input.is_delimited source));
|
|
70 |
|
|
71 |
val keywords = Thy_Header.get_keywords' ctxt;
|
|
72 |
val toks =
|
|
73 |
Source.of_list (Input.source_explode source)
|
|
74 |
|> Token.source' true keywords
|
|
75 |
|> Source.exhaust;
|
|
76 |
val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
|
|
77 |
in
|
|
78 |
implode (map Latex.output_token toks) |>
|
|
79 |
(if Config.get ctxt Thy_Output.display
|
|
80 |
then Latex.environment "isabelle"
|
|
81 |
else enclose "\\isa{" "}")
|
|
82 |
end));
|
|
83 |
|
|
84 |
|
|
85 |
(* goal state *)
|
|
86 |
|
|
87 |
local
|
|
88 |
|
|
89 |
fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
|
|
90 |
(fn {state, context = ctxt, ...} => fn () =>
|
|
91 |
Thy_Output.output ctxt
|
|
92 |
[Goal_Display.pretty_goal
|
|
93 |
(Config.put Goal_Display.show_main_goal main ctxt)
|
|
94 |
(#goal (Proof.goal (Toplevel.proof_of state)))]);
|
|
95 |
|
|
96 |
in
|
|
97 |
|
|
98 |
val _ = Theory.setup
|
|
99 |
(goal_state @{binding goals} true #>
|
|
100 |
goal_state @{binding subgoals} false);
|
|
101 |
|
|
102 |
end;
|
|
103 |
|
|
104 |
|
|
105 |
(* embedded lemma *)
|
|
106 |
|
|
107 |
val _ = Theory.setup
|
|
108 |
(Thy_Output.antiquotation @{binding lemma}
|
|
109 |
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
|
|
110 |
Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
|
|
111 |
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
|
|
112 |
let
|
|
113 |
val prop_src = Token.src (Token.name_of_src source) [prop_token];
|
|
114 |
|
|
115 |
val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
|
|
116 |
val _ = Context_Position.reports ctxt reports;
|
|
117 |
|
|
118 |
(* FIXME check proof!? *)
|
|
119 |
val _ = ctxt
|
|
120 |
|> Proof.theorem NONE (K I) [[(prop, [])]]
|
|
121 |
|> Proof.global_terminal_proof (m1, m2);
|
|
122 |
in
|
|
123 |
Thy_Output.output ctxt
|
|
124 |
(Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop])
|
|
125 |
end));
|
|
126 |
|
|
127 |
|
|
128 |
(* verbatim text *)
|
|
129 |
|
|
130 |
val _ =
|
|
131 |
Theory.setup
|
|
132 |
(Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
|
|
133 |
(Thy_Output.verbatim_text o #context));
|
|
134 |
|
|
135 |
|
|
136 |
(* ML text *)
|
|
137 |
|
|
138 |
local
|
|
139 |
|
|
140 |
fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
|
|
141 |
(fn {context = ctxt, ...} => fn source =>
|
|
142 |
(ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
|
|
143 |
Thy_Output.verbatim_text ctxt (Input.source_content source)));
|
|
144 |
|
|
145 |
fun ml_enclose bg en source =
|
|
146 |
ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
|
|
147 |
|
|
148 |
in
|
|
149 |
|
|
150 |
val _ = Theory.setup
|
|
151 |
(ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
|
|
152 |
ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
|
|
153 |
ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
|
|
154 |
ml_text @{binding ML_structure}
|
|
155 |
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
|
|
156 |
|
|
157 |
ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
|
|
158 |
(fn source =>
|
|
159 |
ML_Lex.read ("ML_Env.check_functor " ^
|
|
160 |
ML_Syntax.print_string (Input.source_content source))) #>
|
|
161 |
|
|
162 |
ml_text @{binding ML_text} (K []));
|
|
163 |
|
|
164 |
end;
|
|
165 |
|
|
166 |
|
|
167 |
(* URLs *)
|
|
168 |
|
|
169 |
val _ = Theory.setup
|
|
170 |
(Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
|
|
171 |
(fn {context = ctxt, ...} => fn (name, pos) =>
|
|
172 |
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
|
|
173 |
enclose "\\url{" "}" name)));
|
|
174 |
|
61623
|
175 |
|
|
176 |
(* formal entities *)
|
|
177 |
|
|
178 |
fun entity_antiquotation name check output =
|
|
179 |
Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
|
|
180 |
(fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
|
|
181 |
|
|
182 |
val _ =
|
|
183 |
Theory.setup
|
|
184 |
(entity_antiquotation @{binding command} Outer_Syntax.check_command
|
|
185 |
(enclose "\\isacommand{" "}" o Output.output) #>
|
|
186 |
entity_antiquotation @{binding method} Method.check_name Output.output #>
|
|
187 |
entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
|
|
188 |
|
61619
|
189 |
end;
|