1(* Title: Pure/ML/ml_pretty.ML 2 Author: Makarius 3 4Minimal support for raw ML pretty printing, notably for toplevel pp. 5*) 6 7signature ML_PRETTY = 8sig 9 datatype pretty = 10 Block of (string * string) * bool * FixedInt.int * pretty list | 11 String of string * FixedInt.int | 12 Break of bool * FixedInt.int * FixedInt.int 13 val block: pretty list -> pretty 14 val str: string -> pretty 15 val brk: FixedInt.int -> pretty 16 val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) -> 17 ('a * 'b) * FixedInt.int -> pretty 18 val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) -> 19 'a list * FixedInt.int -> pretty 20 val to_polyml: pretty -> PolyML_Pretty.pretty 21 val from_polyml: PolyML_Pretty.pretty -> pretty 22 val format_polyml: int -> PolyML_Pretty.pretty -> string 23 val format: int -> pretty -> string 24 val default_margin: int 25 val string_of_polyml: PolyML_Pretty.pretty -> string 26 val make_string_fn: string 27end; 28 29structure ML_Pretty: ML_PRETTY = 30struct 31 32(* datatype pretty *) 33 34datatype pretty = 35 Block of (string * string) * bool * FixedInt.int * pretty list | 36 String of string * FixedInt.int | 37 Break of bool * FixedInt.int * FixedInt.int; 38 39fun block prts = Block (("", ""), false, 2, prts); 40fun str s = String (s, FixedInt.fromInt (size s)); 41fun brk width = Break (false, width, 0); 42 43fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) = 44 block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"]; 45 46fun enum sep lpar rpar pretty (args, depth: FixedInt.int) = 47 let 48 fun elems _ [] = [] 49 | elems 0 _ = [str "..."] 50 | elems d [x] = [pretty (x, d)] 51 | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs; 52 in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end; 53 54 55(* convert *) 56 57fun to_polyml (Break (false, width, offset)) = PolyML_Pretty.PrettyBreak (width, offset) 58 | to_polyml (Break (true, _, _)) = 59 PolyML_Pretty.PrettyBlock (0, false, [PolyML_Pretty.ContextProperty ("fbrk", "")], 60 [PolyML_Pretty.PrettyString " "]) 61 | to_polyml (Block ((bg, en), consistent, ind, prts)) = 62 let val context = 63 (if bg = "" then [] else [PolyML_Pretty.ContextProperty ("begin", bg)]) @ 64 (if en = "" then [] else [PolyML_Pretty.ContextProperty ("end", en)]) 65 in PolyML_Pretty.PrettyBlock (ind, consistent, context, map to_polyml prts) end 66 | to_polyml (String (s, len)) = 67 if len = FixedInt.fromInt (size s) then PolyML_Pretty.PrettyString s 68 else 69 PolyML_Pretty.PrettyBlock 70 (0, false, 71 [PolyML_Pretty.ContextProperty ("length", FixedInt.toString len)], [PolyML_Pretty.PrettyString s]); 72 73val from_polyml = 74 let 75 fun convert _ (PolyML_Pretty.PrettyBreak (width, offset)) = Break (false, width, offset) 76 | convert _ (PolyML_Pretty.PrettyBlock (_, _, 77 [PolyML_Pretty.ContextProperty ("fbrk", _)], [PolyML_Pretty.PrettyString " "])) = 78 Break (true, 1, 0) 79 | convert len (PolyML_Pretty.PrettyBlock (ind, consistent, context, prts)) = 80 let 81 fun property name default = 82 (case List.find (fn PolyML_Pretty.ContextProperty (a, _) => name = a | _ => false) context of 83 SOME (PolyML_Pretty.ContextProperty (_, b)) => b 84 | _ => default); 85 val bg = property "begin" ""; 86 val en = property "end" ""; 87 val len' = property "length" len; 88 in Block ((bg, en), consistent, ind, map (convert len') prts) end 89 | convert len (PolyML_Pretty.PrettyString s) = 90 String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s)) 91 in convert "" end; 92 93 94(* format *) 95 96fun format_polyml margin prt = 97 let 98 val result = Unsynchronized.ref []; 99 val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt 100 in String.concat (List.rev (! result)) end; 101 102fun format margin = format_polyml margin o to_polyml; 103 104val default_margin = 76; 105 106 107(* make string *) 108 109val string_of_polyml = format_polyml default_margin; 110 111val make_string_fn = 112 "(fn x => ML_Pretty.string_of_polyml (ML_system_pretty \ 113 \(x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))))"; 114 115end; 116