# HG changeset patch
# User wenzelm
# Date 1300788873 -3600
# Node ID a7a4e04b538633ce3a02c4baa3db99e35dc302cd
# Parent  6341c23baf109c15a5e4f19543c45f948c756b32
pretty_string: proper handling of negative max_len;

diff -r 6341c23baf10 -r a7a4e04b5386 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Mon Mar 21 23:38:32 2011 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Tue Mar 22 11:14:33 2011 +0100
@@ -106,7 +106,7 @@
         handle Fail _ => Symbol.explode str;
     val body' =
       if length body <= max_len then body
-      else take max_len body @ ["..."];
+      else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_char body'))) end;
 
 end;