tuned ML toplevel pp for type string: observe depth limit;

--- a/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 18:18:42 2010 +0100
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 20:41:33 2010 +0100
@@ -4,6 +4,9 @@
 Extra toplevel pretty-printing for Poly/ML 5.3.0.
 *)
 
+PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
+
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
 

--- a/src/Pure/ML/ml_syntax.ML	Wed Dec 29 18:18:42 2010 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Wed Dec 29 20:41:33 2010 +0100
@@ -26,7 +26,7 @@
   val print_sort: sort -> string
   val print_typ: typ -> string
   val print_term: term -> string
-  val pretty_string: string -> Pretty.T
+  val pretty_string: int -> string -> Pretty.T
 end;
 
 structure ML_Syntax: ML_SYNTAX =
@@ -99,12 +99,14 @@
 
 (* toplevel pretty printing *)
 
-fun pretty_string raw_str =
+fun pretty_string max_len str =
   let
-    val str =
-      implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
-        handle Fail _ => raw_str;
-    val syms = Symbol.explode str;
-  in Pretty.str (quote (implode (map print_char syms))) end;
+    val body =
+      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
+        handle Fail _ => Symbol.explode str;
+    val body' =
+      if length body <= max_len then body
+      else take max_len body @ ["..."];
+  in Pretty.str (quote (implode (map print_char body'))) end;
 
 end;

--- a/src/Pure/pure_setup.ML	Wed Dec 29 18:18:42 2010 +0100
+++ b/src/Pure/pure_setup.ML	Wed Dec 29 20:41:33 2010 +0100
@@ -18,10 +18,6 @@
 
 (* ML toplevel pretty printing *)
 
-if String.isPrefix "polyml" ml_system
-then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
-else ();
-
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";