tuned messages -- avoid text folds stemming from Pretty.chunks;
authorwenzelm
Thu Jul 18 22:32:00 2013 +0200 (2013-07-18)
changeset 52703d68fd63bf082
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
     1.1 --- a/src/Pure/Tools/find_consts.ML	Thu Jul 18 22:18:20 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Thu Jul 18 22:32:00 2013 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4        else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     1.5      Pretty.str "" ::
     1.6      map (pretty_const ctxt) matches
     1.7 -  end |> Pretty.chunks |> Pretty.writeln;
     1.8 +  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
     1.9  
    1.10  
    1.11  (* command syntax *)
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:18:20 2013 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:32:00 2013 +0200
     2.3 @@ -588,7 +588,7 @@
     2.4       else
     2.5        [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
     2.6          grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
     2.7 -  end |> Pretty.chunks |> Pretty.writeln;
     2.8 +  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
     2.9  
    2.10  fun print_theorems ctxt =
    2.11    gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;