1.1 --- a/src/Pure/ML/ml_syntax.ML	Thu Jun 24 22:58:45 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Thu Jun 24 23:20:47 2010 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val print_sort: sort -> string
     1.5    val print_typ: typ -> string
     1.6    val print_term: term -> string
     1.7 +  val pretty_string: string -> Pretty.T
     1.8  end;
     1.9  
    1.10  structure ML_Syntax: ML_SYNTAX =
    1.11 @@ -92,4 +93,15 @@
    1.12        "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    1.13    | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    1.14  
    1.15 +
    1.16 +(* toplevel pretty printing *)
    1.17 +
    1.18 +fun pretty_string raw_str =
    1.19 +  let
    1.20 +    val str =
    1.21 +      implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
    1.22 +        handle Fail _ => raw_str;
    1.23 +    val syms = Symbol.explode str handle ERROR _ => explode str;
    1.24 +  in Pretty.str (quote (implode (map print_char syms))) end;
    1.25 +
    1.26  end;

     2.1 --- a/src/Pure/pure_setup.ML	Thu Jun 24 22:58:45 2010 +0200
     2.2 +++ b/src/Pure/pure_setup.ML	Thu Jun 24 23:20:47 2010 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4  
     2.5  (* ML toplevel pretty printing *)
     2.6  
     2.7 +toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
     2.8  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
     2.9  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    2.10  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";