pretty_string: proper handling of negative max_len;
authorwenzelm
Tue Mar 22 11:14:33 2011 +0100 (2011-03-22)
changeset 42047a7a4e04b5386
parent 42046 6341c23baf10
child 42048 afd11ca8e018
pretty_string: proper handling of negative max_len;
src/Pure/ML/ml_syntax.ML
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Mon Mar 21 23:38:32 2011 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Tue Mar 22 11:14:33 2011 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4          handle Fail _ => Symbol.explode str;
     1.5      val body' =
     1.6        if length body <= max_len then body
     1.7 -      else take max_len body @ ["..."];
     1.8 +      else take (Int.max (max_len, 0)) body @ ["..."];
     1.9    in Pretty.str (quote (implode (map print_char body'))) end;
    1.10  
    1.11  end;