1.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 02 16:53:23 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 16:53:23 2010 +0200
     1.3 @@ -127,7 +127,8 @@
     1.4  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
     1.5  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
     1.6  
     1.7 -fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
     1.8 +fun markup_stmt name = Print_Mode.setmp [code_presentationN]
     1.9 +  (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
    1.10  
    1.11  fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
    1.12        implode (map (filter_presentation presentation_names