tuned message -- more context for detached window etc.;
authorwenzelm
Wed May 07 10:24:32 2014 +0200 (2014-05-07)
changeset 5689148899c43b07d
parent 56890 7f120d227ca5
child 56892 1c7552b05466
tuned message -- more context for detached window etc.;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed May 07 10:13:31 2014 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed May 07 10:24:32 2014 +0200
     1.3 @@ -113,7 +113,9 @@
     1.4        |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
     1.5        |> map (apsnd fst o snd);
     1.6    in
     1.7 -    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
     1.8 +    Pretty.block
     1.9 +      (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
    1.10 +        Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
    1.11      Pretty.str "" ::
    1.12      Pretty.str
    1.13       (if null matches
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Wed May 07 10:13:31 2014 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed May 07 10:24:32 2014 +0200
     2.3 @@ -483,7 +483,9 @@
     2.4               then " (" ^ string_of_int returned ^ " displayed)"
     2.5               else ""));
     2.6    in
     2.7 -    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     2.8 +    Pretty.block
     2.9 +      (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
    2.10 +        Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
    2.11      Pretty.str "" ::
    2.12      (if null theorems then [Pretty.str "nothing found"]
    2.13       else