# HG changeset patch
# User wenzelm
# Date 1445106432 -7200
# Node ID e16649b70107c189e52048512b329e719bb6eac8
# Parent  77c9643a6353abf4c624e3f3fb08a3f244536bc2
clarified Latex.environment;

diff -r 77c9643a6353 -r e16649b70107 src/Doc/antiquote_setup.ML
--- 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) ^
diff -r 77c9643a6353 -r e16649b70107 src/Pure/Thy/latex.ML
--- 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
diff -r 77c9643a6353 -r e16649b70107 src/Pure/Thy/thy_output.ML
--- 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{" "}") #>
diff -r 77c9643a6353 -r e16649b70107 src/Pure/Tools/rail.ML
--- 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