added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

--- a/NEWS	Fri Apr 16 10:15:00 2010 +0200
+++ b/NEWS	Fri Apr 16 10:52:10 2010 +0200
@@ -298,6 +298,10 @@
 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
 syntax constant (cf. 'syntax' command).
 
+* Antiquotation @{make_string} inlines a function to print arbitrary
+values similar to the ML toplevel.  The result is compiler dependent
+and may fall back on "?" in certain situations.
+
 * Renamed old-style Drule.standard to Drule.export_without_context, to
 emphasize that this is in no way a standard operation.
 INCOMPATIBILITY.

--- a/src/Pure/ML-Systems/polyml.ML	Fri Apr 16 10:15:00 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Apr 16 10:52:10 2010 +0200
@@ -66,3 +66,6 @@
   use_text context (1, "pp") false
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
+val ml_make_string =
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
+

--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 16 10:15:00 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 16 10:52:10 2010 +0200
@@ -55,7 +55,7 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
-(* print depth *)
+(* toplevel printing *)
 
 local
   val depth = Unsynchronized.ref 10;
@@ -66,6 +66,8 @@
 
 val error_depth = PolyML.error_depth;
 
+val ml_make_string = "PolyML.makestring";
+
 
 
 (** interrupts **)

--- a/src/Pure/ML-Systems/smlnj.ML	Fri Apr 16 10:15:00 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Apr 16 10:52:10 2010 +0200
@@ -61,6 +61,8 @@
     Control.Print.printLength := dest_int n);
 end;
 
+val ml_make_string = "(fn _ => \"?\")";
+
 
 (*prompts*)
 fun ml_prompts p1 p2 =

--- a/src/Pure/ML/ml_antiquote.ML	Fri Apr 16 10:15:00 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Apr 16 10:52:10 2010 +0200
@@ -59,6 +59,8 @@
 
 structure P = OuterParse;
 
+val _ = inline "make_string" (Scan.succeed ml_make_string);
+
 val _ = value "binding"
   (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));