# HG changeset patch
# User wenzelm
# Date 1333977052 -7200
# Node ID 296b478df14e81f90122f6261676c582520032f1
# Parent  84d8952b5bd97f916c89d3511ca49f0184225e39
added ML pretty-printing;

diff -r 84d8952b5bd9 -r 296b478df14e src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Sat Apr 07 20:35:01 2012 +0200
+++ b/src/Pure/General/linear_set.ML	Mon Apr 09 15:10:52 2012 +0200
@@ -18,6 +18,7 @@
   val update: key * 'a -> 'a T -> 'a T
   val iterate: key option ->
     ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
+  val dest: 'a T -> (key * 'a) list
   val get_after: 'a T -> key option -> key option
   val insert_after: key option -> key * 'a -> 'a T -> 'a T
   val delete_after: key option -> 'a T -> 'a T
@@ -94,6 +95,8 @@
           end;
   in apply NONE (optional_start set opt_start) end;
 
+fun dest set = rev (iterate NONE (fn ((_, key), x) => SOME o cons (key, x)) set []);
+
 
 (* relative addressing *)
 
@@ -129,5 +132,15 @@
               |> del_entry key2;
           in (start, entries') end)));
 
+
+(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
+    ml_pretty
+      (ML_Pretty.enum "," "{" "}"
+        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (dest set, depth)));
+
 end;