equal
deleted
inserted
replaced
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 ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
23 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
24 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
24 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
25 else |
25 else |
26 (*map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))*) |
26 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
27 map (Output.output o Pretty.str_of) |
|
28 #> space_implode "\\isasep\\isanewline%\n" |
27 #> space_implode "\\isasep\\isanewline%\n" |
29 #> enclose "\\isa{" "}"); |
28 #> enclose "\\isa{" "}"); |
30 |
29 |
31 val _ = ThyOutput.add_options |
30 val _ = ThyOutput.add_options |
32 [("gray", Library.setmp gray o boolean)] |
31 [("gray", Library.setmp gray o boolean)] |