ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);

--- a/src/Pure/ML/ml_syntax.ML	Thu Jun 24 22:58:45 2010 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Jun 24 23:20:47 2010 +0200
@@ -26,6 +26,7 @@
   val print_sort: sort -> string
   val print_typ: typ -> string
   val print_term: term -> string
+  val pretty_string: string -> Pretty.T
 end;
 
 structure ML_Syntax: ML_SYNTAX =
@@ -92,4 +93,15 @@
       "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
   | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
 
+
+(* toplevel pretty printing *)
+
+fun pretty_string raw_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 handle ERROR _ => explode str;
+  in Pretty.str (quote (implode (map print_char syms))) end;
+
 end;

--- a/src/Pure/pure_setup.ML	Thu Jun 24 22:58:45 2010 +0200
+++ b/src/Pure/pure_setup.ML	Thu Jun 24 23:20:47 2010 +0200
@@ -18,6 +18,7 @@
 
 (* ML toplevel pretty printing *)
 
+toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
 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";