1.1 --- a/src/Pure/General/pretty.ML	Sat Mar 21 15:08:00 2009 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Mar 21 15:08:00 2009 +0100
     1.3 @@ -49,6 +49,7 @@
     1.4    val commas: T list -> T list
     1.5    val enclose: string -> string -> T list -> T
     1.6    val enum: string -> string -> string -> T list -> T
     1.7 +  val position: Position.T -> T
     1.8    val list: string -> string -> T list -> T
     1.9    val str_list: string -> string -> string list -> T
    1.10    val big_list: string -> T list -> T
    1.11 @@ -58,6 +59,8 @@
    1.12    val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    1.13    val setdepth: int -> unit
    1.14    val pprint: T -> pprint_args -> unit
    1.15 +  val to_ML: T -> ML_Pretty.pretty
    1.16 +  val from_ML: ML_Pretty.pretty -> T
    1.17    val symbolicN: string
    1.18    val output_buffer: T -> Buffer.T
    1.19    val output: T -> output
    1.20 @@ -159,6 +162,9 @@
    1.21  
    1.22  fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
    1.23  
    1.24 +val position =
    1.25 +  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
    1.26 +
    1.27  val list = enum ",";
    1.28  fun str_list lpar rpar strs = list lpar rpar (map str strs);
    1.29  
    1.30 @@ -333,6 +339,15 @@
    1.31        | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
    1.32    in pp (prune prt) end;
    1.33  
    1.34 +fun to_ML (Block (_, prts, ind, _)) = ML_Pretty.PrettyBlock (ind, false, [], map to_ML prts)
    1.35 +  | to_ML (String (s, _)) = ML_Pretty.PrettyString s
    1.36 +  | to_ML (Break (false, wd)) = ML_Pretty.PrettyBreak (wd, 0)
    1.37 +  | to_ML (Break (true, _)) = ML_Pretty.PrettyBreak (99999, 0);
    1.38 +
    1.39 +fun from_ML (ML_Pretty.PrettyBlock (ind, _, _, prts)) = blk (ind, map from_ML prts) (* FIXME markup *)
    1.40 +  | from_ML (ML_Pretty.PrettyString s) = String (s, size s)   (* FIXME proper length *)
    1.41 +  | from_ML (ML_Pretty.PrettyBreak (wd, _)) = if wd >= 99999 then fbrk else brk wd;
    1.42 +
    1.43  
    1.44  (* output interfaces *)
    1.45