# HG changeset patch
# User wenzelm
# Date 1399451072 -7200
# Node ID 48899c43b07dc665f0d96a6e8deef0f9aa8303c4
# Parent  7f120d227ca578acbb594ecc2321e5099733efed
tuned message -- more context for detached window etc.;

diff -r 7f120d227ca5 -r 48899c43b07d src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed May 07 10:13:31 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed May 07 10:24:32 2014 +0200
@@ -113,7 +113,9 @@
       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
       |> map (apsnd fst o snd);
   in
-    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+    Pretty.block
+      (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+        Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
     Pretty.str "" ::
     Pretty.str
      (if null matches
diff -r 7f120d227ca5 -r 48899c43b07d src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed May 07 10:13:31 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed May 07 10:24:32 2014 +0200
@@ -483,7 +483,9 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
   in
-    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+    Pretty.block
+      (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+        Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
     Pretty.str "" ::
     (if null theorems then [Pretty.str "nothing found"]
      else