--- a/src/Tools/Code/code_printer.ML Fri Sep 24 14:03:43 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Sep 24 14:03:44 2010 +0200
@@ -133,7 +133,6 @@
fun filter_presentation [] tree =
Buffer.empty
|> fold XML.add_content tree
- |> Buffer.add "\n"
| filter_presentation presentation_names tree =
let
fun is_selected (name, attrs) =
@@ -153,6 +152,7 @@
Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
#> YXML.parse_body
#> filter_presentation presentation_names
+ #> Buffer.add "\n"
#> Buffer.content;