added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);

--- a/src/Pure/General/table.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/General/table.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -392,6 +392,16 @@
 fun merge_list eq = join (fn _ => Library.merge eq);
 
 
+(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
+    ml_pretty
+      (ML_Pretty.enum "," "{" "}"
+        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (dest tab, depth)));
+
+
 (*final declarations of this structure!*)
 fun map f = map_table (K f);
 val map' = map_table;

--- a/src/Pure/IsaMakefile	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/IsaMakefile	Mon Aug 23 15:11:41 2010 +0200
@@ -32,6 +32,7 @@
   ML-Systems/polyml-5.2.ML				\
   ML-Systems/polyml.ML					\
   ML-Systems/polyml_common.ML				\
+  ML-Systems/pp_dummy.ML				\
   ML-Systems/pp_polyml.ML				\
   ML-Systems/proper_int.ML				\
   ML-Systems/single_assignment.ML			\

--- a/src/Pure/ML-Systems/ml_pretty.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/ML-Systems/ml_pretty.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/ml_pretty.ML
     Author:     Makarius
 
-Raw datatype for ML pretty printing.
+Minimal support for raw ML pretty printing -- for boot-strapping only.
 *)
 
 structure ML_Pretty =
@@ -12,5 +12,20 @@
   String of string * int |
   Break of bool * int;
 
+fun block prts = Block (("", ""), prts, 2);
+fun str s = String (s, size s);
+fun brk wd = Break (false, wd);
+
+fun pair pretty1 pretty2 ((x, y), depth: int) =
+  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth) =
+  let
+    fun elems _ [] = []
+      | elems 0 _ = [str "..."]
+      | elems d [x] = [pretty (x, d)]
+      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
+
 end;
 

--- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -25,4 +25,5 @@
 
 use "ML-Systems/compiler_polyml-5.2.ML";
 use "ML-Systems/pp_polyml.ML";
+use "ML-Systems/pp_dummy.ML";
 

--- a/src/Pure/ML-Systems/polyml-5.2.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -27,4 +27,5 @@
 
 use "ML-Systems/compiler_polyml-5.2.ML";
 use "ML-Systems/pp_polyml.ML";
+use "ML-Systems/pp_dummy.ML";
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/pp_dummy.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/pp_dummy.ML
+
+Dummy setup for toplevel pretty printing.
+*)
+
+fun ml_pretty _ = raise Fail "ml_pretty dummy";
+fun pretty_ml _ = raise Fail "pretty_ml dummy";
+
+structure PolyML =
+struct
+  fun addPrettyPrinter _ = ();
+  fun prettyRepresentation _ =
+    raise Fail "PolyML.prettyRepresentation dummy";
+  open PolyML;
+end;
+

--- a/src/Pure/ML-Systems/smlnj.ML	Mon Aug 23 12:06:47 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Aug 23 15:11:41 2010 +0200
@@ -18,6 +18,8 @@
 use "ML-Systems/bash.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+structure PolyML = struct end;
+use "ML-Systems/pp_dummy.ML";
 use "ML-Systems/use_context.ML";