# 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 **)