# HG changeset patch
# User wenzelm
# Date 1374179520 -7200
# Node ID d68fd63bf082f24cbadd55beff828906823c69a6
# Parent  c503730efae539090ee2d669c32eaf622d3adb61
tuned messages -- avoid text folds stemming from Pretty.chunks;

diff -r c503730efae5 -r d68fd63bf082 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Thu Jul 18 22:18:20 2013 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu Jul 18 22:32:00 2013 +0200
@@ -121,7 +121,7 @@
       else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     Pretty.str "" ::
     map (pretty_const ctxt) matches
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
 
 
 (* command syntax *)
diff -r c503730efae5 -r d68fd63bf082 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:18:20 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:32:00 2013 +0200
@@ -588,7 +588,7 @@
      else
       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
         grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
-  end |> Pretty.chunks |> Pretty.writeln;
+  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
 
 fun print_theorems ctxt =
   gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;