author  wenzelm 
Thu, 21 Jun 2018 14:29:44 +0200  
changeset 68481  fb6afa538b04 
parent 67569  5d71b114e7a3 
child 68482  cb84beb84ca9 
permissions  rwrr 
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 leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

95 
(* Markdown errors *) 
df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

96 

df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

97 
local 
df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

98 

df566b87e269
more explicit errors for control symbols that are leftover 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 leftover 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 leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

104 

df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

105 
in 
df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

106 

df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

107 
val _ = 
df566b87e269
more explicit errors for control symbols that are leftover 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 leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

112 

df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

113 
end; 
df566b87e269
more explicit errors for control symbols that are leftover after Markdown parsing;
wenzelm
parents:
62058
diff
changeset

114 

df566b87e269
more explicit errors for control symbols that are leftover 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 
(* quasiformal 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; 