# HG changeset patch
# User wenzelm
# Date 1293659493 -3600
# Node ID e228a2e5a0262b0a2f6fbb6c19c234a4e706db67
# Parent  b6dc60638be05dae7a49202e6c77b54e4f5877e1# Parent  a2208d3e2bd65fed8a0b9c1cd75eec7244d86faf
merged

diff -r b6dc60638be0 -r e228a2e5a026 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Dec 29 21:52:44 2010 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Dec 29 22:51:33 2010 +0100
@@ -174,9 +174,11 @@
   in (implode syms', range syms') end;
 
 fun explode (str, pos) =
-  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
-    (Symbol.explode str) (Position.reset_range pos)
-  |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
+  let
+    val (res, _) =
+      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
+        (Symbol.explode str) ([], Position.reset_range pos);
+  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
 
 end;
 
diff -r b6dc60638be0 -r e228a2e5a026 src/Pure/ML/install_pp_polyml-5.3.ML
--- a/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 21:52:44 2010 +0100
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Wed Dec 29 22:51: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));
 
diff -r b6dc60638be0 -r e228a2e5a026 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Wed Dec 29 21:52:44 2010 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Wed Dec 29 22:51: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;
diff -r b6dc60638be0 -r e228a2e5a026 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Wed Dec 29 21:52:44 2010 +0100
+++ b/src/Pure/pure_setup.ML	Wed Dec 29 22:51: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";