tuned messages -- avoid text folds stemming from Pretty.chunks;
authorwenzelm
Thu, 18 Jul 2013 22:32:00 +0200
changeset 52703 d68fd63bf082
parent 52702 c503730efae5
child 52704 b824497c8e86
tuned messages -- avoid text folds stemming from Pretty.chunks;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.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 *)
--- 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;