equal
deleted
inserted
replaced
118 Pretty.str |
118 Pretty.str |
119 (if null matches |
119 (if null matches |
120 then "nothing found" |
120 then "nothing found" |
121 else "found " ^ string_of_int (length matches) ^ " constant(s):") :: |
121 else "found " ^ string_of_int (length matches) ^ " constant(s):") :: |
122 Pretty.str "" :: |
122 Pretty.str "" :: |
123 map (Pretty.item o single o pretty_const ctxt) matches |
123 grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches |
124 end |> Pretty.fbreaks |> curry Pretty.blk 0; |
124 end |> Pretty.fbreaks |> curry Pretty.blk 0; |
125 |
125 |
126 fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args); |
126 fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args); |
127 |
127 |
128 |
128 |