pretty_string: proper handling of negative max_len;

--- 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;