src/Tools/Code/code_printer.ML
changeset 39069 371976383ac0
parent 39062 9eb380ecf155
child 39531 49194c9b0dd4
equal deleted inserted replaced
39068:5ac590e8b320 39069:371976383ac0
   125   | enum_default default sep l r xs = enum sep l r xs;
   125   | enum_default default sep l r xs = enum sep l r xs;
   126 fun semicolon ps = Pretty.block [concat ps, str ";"];
   126 fun semicolon ps = Pretty.block [concat ps, str ";"];
   127 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   127 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   128 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   128 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   129 
   129 
   130 fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
   130 fun markup_stmt name = Print_Mode.setmp [code_presentationN]
       
   131   (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
   131 
   132 
   132 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
   133 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
   133       implode (map (filter_presentation presentation_names
   134       implode (map (filter_presentation presentation_names
   134         (selected orelse (name = code_presentationN
   135         (selected orelse (name = code_presentationN
   135           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
   136           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)