src/Pure/Tools/find_consts.ML
changeset 56908 734f7e6151c9
parent 56891 48899c43b07d
child 56912 293cd4dcfebc
     1.1 --- a/src/Pure/Tools/find_consts.ML	Thu May 08 11:47:38 2014 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Thu May 08 13:47:17 2014 +0200
     1.3 @@ -114,15 +114,12 @@
     1.4        |> map (apsnd fst o snd);
     1.5    in
     1.6      Pretty.block
     1.7 -      (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
     1.8 -        Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
     1.9 +      (Pretty.fbreaks (Pretty.keyword1 "find_consts" :: map pretty_criterion raw_criteria)) ::
    1.10      Pretty.str "" ::
    1.11 -    Pretty.str
    1.12 -     (if null matches
    1.13 -      then "nothing found"
    1.14 -      else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
    1.15 -    Pretty.str "" ::
    1.16 -    grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches
    1.17 +    (if null matches then [Pretty.str "found nothing"]
    1.18 +     else
    1.19 +       Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
    1.20 +       grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
    1.21    end |> Pretty.fbreaks |> curry Pretty.blk 0;
    1.22  
    1.23  fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);