clarified Latex.environment;
authorwenzelm
Sat Oct 17 20:27:12 2015 +0200 (2015-10-17)
changeset 61462e16649b70107
parent 61461 77c9643a6353
child 61463 8e46cea6a45a
clarified Latex.environment;
src/Doc/antiquote_setup.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Oct 17 19:47:34 2015 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sat Oct 17 20:27:12 2015 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4                    (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
     1.5                "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
     1.6              #> space_implode "\\par\\smallskip%\n"
     1.7 -            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
     1.8 +            #> Latex.environment "isabelle"
     1.9            else
    1.10              map (fn (p, name) =>
    1.11                Output.output (Pretty.str_of p) ^
     2.1 --- a/src/Pure/Thy/latex.ML	Sat Oct 17 19:47:34 2015 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Sat Oct 17 20:27:12 2015 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    val end_delim: string -> string
     2.5    val begin_tag: string -> string
     2.6    val end_tag: string -> string
     2.7 +  val environment: string -> string -> string
     2.8    val tex_trailer: string
     2.9    val isabelle_theory: string -> string -> string
    2.10    val symbol_source: (string -> bool) * (string -> bool) ->
    2.11 @@ -154,6 +155,9 @@
    2.12  
    2.13  (* theory presentation *)
    2.14  
    2.15 +fun environment name =
    2.16 +  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}%\n");
    2.17 +
    2.18  val tex_trailer =
    2.19    "%%% Local Variables:\n\
    2.20    \%%% mode: latex\n\
    2.21 @@ -163,7 +167,7 @@
    2.22  fun isabelle_theory name txt =
    2.23    "%\n\\begin{isabellebody}%\n\
    2.24    \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    2.25 -  "\\end{isabellebody}%\n" ^ tex_trailer;
    2.26 +  "%\n\\end{isabellebody}%\n" ^ tex_trailer;
    2.27  
    2.28  fun symbol_source known name syms =
    2.29    isabelle_theory name
     3.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:47:34 2015 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 20:27:12 2015 +0200
     3.3 @@ -199,11 +199,7 @@
     3.4      fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
     3.5      and output_block (Markdown.Paragraph lines) = cat_lines (map output_line lines)
     3.6        | output_block (Markdown.List {kind, body, ...}) =
     3.7 -          let val env = Markdown.print_kind kind in
     3.8 -            "%\n\\begin{" ^ env ^ "}%\n" ^
     3.9 -            output_blocks body ^
    3.10 -            "%\n\\end{" ^ env ^ "}%\n"
    3.11 -          end;
    3.12 +          Latex.environment (Markdown.print_kind kind) (output_blocks body);
    3.13    in
    3.14      if Toplevel.is_skipped_proof state then ""
    3.15      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    3.16 @@ -254,9 +250,7 @@
    3.17    | Markup_Token (cmd, source) =>
    3.18        "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
    3.19    | Markup_Env_Token (cmd, source) =>
    3.20 -      "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    3.21 -      output_text state {markdown = true} source ^
    3.22 -      "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    3.23 +      Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
    3.24    | Raw_Token source =>
    3.25        "%\n" ^ output_text state {markdown = true} source ^ "\n");
    3.26  
    3.27 @@ -591,7 +585,7 @@
    3.28    |> (if Config.get ctxt display then
    3.29          map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
    3.30          #> space_implode "\\isasep\\isanewline%\n"
    3.31 -        #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    3.32 +        #> Latex.environment "isabelle"
    3.33        else
    3.34          map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
    3.35            Output.output)
    3.36 @@ -682,8 +676,7 @@
    3.37  
    3.38  fun verbatim_text ctxt =
    3.39    if Config.get ctxt display then
    3.40 -    Latex.output_ascii #>
    3.41 -    enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
    3.42 +    Latex.output_ascii #> Latex.environment "isabellett"
    3.43    else
    3.44      split_lines #>
    3.45      map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
     4.1 --- a/src/Pure/Tools/rail.ML	Sat Oct 17 19:47:34 2015 +0200
     4.2 +++ b/src/Pure/Tools/rail.ML	Sat Oct 17 20:27:12 2015 +0200
     4.3 @@ -354,11 +354,7 @@
     4.4          output "" rail' ^
     4.5          "\\rail@end\n"
     4.6        end;
     4.7 -  in
     4.8 -    "\\begin{railoutput}\n" ^
     4.9 -    implode (map output_rule rules) ^
    4.10 -    "\\end{railoutput}\n"
    4.11 -  end;
    4.12 +  in Latex.environment "railoutput" (implode (map output_rule rules)) end;
    4.13  
    4.14  in
    4.15