Added a few breaks in error text.
authornipkow
Fri Oct 09 14:19:13 1998 +0200 (1998-10-09)
changeset 5633fb7fa1b154c4
parent 5632 5682dce02591
child 5634 7f61a83d4a01
Added a few breaks in error text.
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Oct 09 11:27:11 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 09 14:19:13 1998 +0200
     1.3 @@ -605,10 +605,12 @@
     1.4          val text = cat_lines
     1.5           ["Type error in application: " ^ why,
     1.6            "",
     1.7 -          Pretty.string_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
     1.8 -            Pretty.str " :: ", prT T]),
     1.9 -          Pretty.string_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.10 -            Pretty.str " :: ", prT U]), ""];
    1.11 +          Pretty.string_of
    1.12 +           (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    1.13 +                          Pretty.str " ::", Pretty.brk 1, prT T]),
    1.14 +          Pretty.string_of
    1.15 +           (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.16 +                          Pretty.str " ::", Pretty.brk 1, prT U]), ""];
    1.17        in raise TYPE (text, [T, U], [t', u']) end;
    1.18  
    1.19      fun typ_of (_, Const (_, T)) = T