src/Pure/ML/ml_syntax.ML
changeset 42047 a7a4e04b5386
parent 41491 a2ad5b824051
child 42290 b1f544c84040
--- 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;