tuned message: more compact, imitate actual command line;
authorwenzelm
Thu May 08 13:47:17 2014 +0200 (2014-05-08)
changeset 56908734f7e6151c9
parent 56907 0f3c375fd27c
child 56909 a1557dc7f589
tuned message: more compact, imitate actual command line;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     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);
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Thu May 08 11:47:38 2014 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu May 08 13:47:17 2014 +0200
     2.3 @@ -484,13 +484,12 @@
     2.4               else ""));
     2.5    in
     2.6      Pretty.block
     2.7 -      (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
     2.8 -        Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
     2.9 +      (Pretty.fbreaks (Pretty.keyword1 "find_theorems" :: map (pretty_criterion ctxt) criteria)) ::
    2.10      Pretty.str "" ::
    2.11 -    (if null theorems then [Pretty.str "nothing found"]
    2.12 +    (if null theorems then [Pretty.str "found nothing"]
    2.13       else
    2.14 -      [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
    2.15 -        grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
    2.16 +       Pretty.str (tally_msg ^ ":") ::
    2.17 +       grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
    2.18    end |> Pretty.fbreaks |> curry Pretty.blk 0;
    2.19  
    2.20  end;