# HG changeset patch
# User haftmann
# Date 1285329824 -7200
# Node ID d9fb92a8c80a2cd829f9fdfae08a01ddf67936e0
# Parent  e9f89d86c9632333007ec905e937ae1bda2ae347
always add trailing newline for presentation

diff -r e9f89d86c963 -r d9fb92a8c80a src/Tools/Code/code_printer.ML
--- 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;