added position;
added to_ML, from_ML (approximation);

--- a/src/Pure/General/pretty.ML	Sat Mar 21 15:08:00 2009 +0100
+++ b/src/Pure/General/pretty.ML	Sat Mar 21 15:08:00 2009 +0100
@@ -49,6 +49,7 @@
   val commas: T list -> T list
   val enclose: string -> string -> T list -> T
   val enum: string -> string -> string -> T list -> T
+  val position: Position.T -> T
   val list: string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
@@ -58,6 +59,8 @@
   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
   val setdepth: int -> unit
   val pprint: T -> pprint_args -> unit
+  val to_ML: T -> ML_Pretty.pretty
+  val from_ML: ML_Pretty.pretty -> T
   val symbolicN: string
   val output_buffer: T -> Buffer.T
   val output: T -> output
@@ -159,6 +162,9 @@
 
 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
 
+val position =
+  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+
 val list = enum ",";
 fun str_list lpar rpar strs = list lpar rpar (map str strs);
 
@@ -333,6 +339,15 @@
       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   in pp (prune prt) end;
 
+fun to_ML (Block (_, prts, ind, _)) = ML_Pretty.PrettyBlock (ind, false, [], map to_ML prts)
+  | to_ML (String (s, _)) = ML_Pretty.PrettyString s
+  | to_ML (Break (false, wd)) = ML_Pretty.PrettyBreak (wd, 0)
+  | to_ML (Break (true, _)) = ML_Pretty.PrettyBreak (99999, 0);
+
+fun from_ML (ML_Pretty.PrettyBlock (ind, _, _, prts)) = blk (ind, map from_ML prts) (* FIXME markup *)
+  | from_ML (ML_Pretty.PrettyString s) = String (s, size s)   (* FIXME proper length *)
+  | from_ML (ML_Pretty.PrettyBreak (wd, _)) = if wd >= 99999 then fbrk else brk wd;
+
 
 (* output interfaces *)