# HG changeset patch
# User haftmann
# Date 1283436853 -7200
# Node ID 9eb380ecf1550de908e22920ccda1c61232b0a90
# Parent  9b1fd2df743c9392c4417969e08d9a63f0c83e4d
corrected printmode handling

diff -r 9b1fd2df743c -r 9eb380ecf155 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Sep 02 16:14:13 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 16:14:13 2010 +0200
@@ -128,6 +128,7 @@
 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
 
 fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
+
 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
       implode (map (filter_presentation presentation_names
         (selected orelse (name = code_presentationN
@@ -145,13 +146,15 @@
         else s1 ^ s ^ s2
       end;
 
-fun format presentation_names width p =
-  if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
-  else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
-    |> YXML.parse_body
-    |> tap (fn ts => tracing (cat_lines (map XML.string_of ts)))
-    |> maps_string "\n\n" (filter_presentation presentation_names false)
-    |> suffix "\n"
+fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs)
+  | plain_text (XML.Text s) = s
+
+fun format presentation_names width =
+  Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
+  #> YXML.parse_body
+  #> (if null presentation_names then implode o map plain_text
+      else maps_string "\n\n" (filter_presentation presentation_names false))
+  #> suffix "\n";
 
 
 (** names and variable name contexts **)