--- a/src/Doc/antiquote_setup.ML Sat Oct 17 19:47:34 2015 +0200
+++ b/src/Doc/antiquote_setup.ML Sat Oct 17 20:27:12 2015 +0200
@@ -132,7 +132,7 @@
(Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
"\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ #> Latex.environment "isabelle"
else
map (fn (p, name) =>
Output.output (Pretty.str_of p) ^
--- a/src/Pure/Thy/latex.ML Sat Oct 17 19:47:34 2015 +0200
+++ b/src/Pure/Thy/latex.ML Sat Oct 17 20:27:12 2015 +0200
@@ -16,6 +16,7 @@
val end_delim: string -> string
val begin_tag: string -> string
val end_tag: string -> string
+ val environment: string -> string -> string
val tex_trailer: string
val isabelle_theory: string -> string -> string
val symbol_source: (string -> bool) * (string -> bool) ->
@@ -154,6 +155,9 @@
(* theory presentation *)
+fun environment name =
+ enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}%\n");
+
val tex_trailer =
"%%% Local Variables:\n\
\%%% mode: latex\n\
@@ -163,7 +167,7 @@
fun isabelle_theory name txt =
"%\n\\begin{isabellebody}%\n\
\\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
- "\\end{isabellebody}%\n" ^ tex_trailer;
+ "%\n\\end{isabellebody}%\n" ^ tex_trailer;
fun symbol_source known name syms =
isabelle_theory name
--- a/src/Pure/Thy/thy_output.ML Sat Oct 17 19:47:34 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat Oct 17 20:27:12 2015 +0200
@@ -199,11 +199,7 @@
fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
and output_block (Markdown.Paragraph lines) = cat_lines (map output_line lines)
| output_block (Markdown.List {kind, body, ...}) =
- let val env = Markdown.print_kind kind in
- "%\n\\begin{" ^ env ^ "}%\n" ^
- output_blocks body ^
- "%\n\\end{" ^ env ^ "}%\n"
- end;
+ Latex.environment (Markdown.print_kind kind) (output_blocks body);
in
if Toplevel.is_skipped_proof state then ""
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
@@ -254,9 +250,7 @@
| Markup_Token (cmd, source) =>
"%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
| Markup_Env_Token (cmd, source) =>
- "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
- output_text state {markdown = true} source ^
- "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
+ Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
| Raw_Token source =>
"%\n" ^ output_text state {markdown = true} source ^ "\n");
@@ -591,7 +585,7 @@
|> (if Config.get ctxt display then
map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
#> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ #> Latex.environment "isabelle"
else
map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
Output.output)
@@ -682,8 +676,7 @@
fun verbatim_text ctxt =
if Config.get ctxt display then
- Latex.output_ascii #>
- enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
+ Latex.output_ascii #> Latex.environment "isabellett"
else
split_lines #>
map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
--- a/src/Pure/Tools/rail.ML Sat Oct 17 19:47:34 2015 +0200
+++ b/src/Pure/Tools/rail.ML Sat Oct 17 20:27:12 2015 +0200
@@ -354,11 +354,7 @@
output "" rail' ^
"\\rail@end\n"
end;
- in
- "\\begin{railoutput}\n" ^
- implode (map output_rule rules) ^
- "\\end{railoutput}\n"
- end;
+ in Latex.environment "railoutput" (implode (map output_rule rules)) end;
in