src/Tools/Code/code_printer.ML
changeset 39062 9eb380ecf155
parent 39057 c6d146ed07ae
child 39069 371976383ac0
equal deleted inserted replaced
39061:9b1fd2df743c 39062:9eb380ecf155
   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 = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
       
   131 
   131 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
   132 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
   132       implode (map (filter_presentation presentation_names
   133       implode (map (filter_presentation presentation_names
   133         (selected orelse (name = code_presentationN
   134         (selected orelse (name = code_presentationN
   134           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
   135           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
   135   | filter_presentation presentation_names selected (XML.Text s) =
   136   | filter_presentation presentation_names selected (XML.Text s) =
   143       in if s1 = "" then s2
   144       in if s1 = "" then s2
   144         else if s2 = "" then s1
   145         else if s2 = "" then s1
   145         else s1 ^ s ^ s2
   146         else s1 ^ s ^ s2
   146       end;
   147       end;
   147 
   148 
   148 fun format presentation_names width p =
   149 fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs)
   149   if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
   150   | plain_text (XML.Text s) = s
   150   else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
   151 
   151     |> YXML.parse_body
   152 fun format presentation_names width =
   152     |> tap (fn ts => tracing (cat_lines (map XML.string_of ts)))
   153   Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
   153     |> maps_string "\n\n" (filter_presentation presentation_names false)
   154   #> YXML.parse_body
   154     |> suffix "\n"
   155   #> (if null presentation_names then implode o map plain_text
       
   156       else maps_string "\n\n" (filter_presentation presentation_names false))
       
   157   #> suffix "\n";
   155 
   158 
   156 
   159 
   157 (** names and variable name contexts **)
   160 (** names and variable name contexts **)
   158 
   161 
   159 type var_ctxt = string Symtab.table * Name.context;
   162 type var_ctxt = string Symtab.table * Name.context;