equal
deleted
inserted
replaced
18 |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
18 |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
19 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
19 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
20 |> (if ! ThyOutput.display then |
20 |> (if ! ThyOutput.display then |
21 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
21 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
22 #> space_implode "\\isasep\\isanewline%\n" |
22 #> space_implode "\\isasep\\isanewline%\n" |
|
23 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
23 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
24 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
24 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
|
25 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
25 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
26 else |
26 else |
27 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
27 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
28 #> space_implode "\\isasep\\isanewline%\n" |
28 #> space_implode "\\isasep\\isanewline%\n" |
29 #> enclose "\\isa{" "}"); |
29 #> enclose "\\isa{" "}"); |