equal
deleted
inserted
replaced
74 val block_enclose: T * T -> T list -> T |
74 val block_enclose: T * T -> T list -> T |
75 val writeln_chunks: T list -> unit |
75 val writeln_chunks: T list -> unit |
76 val writeln_chunks2: T list -> unit |
76 val writeln_chunks2: T list -> unit |
77 val to_ML: FixedInt.int -> T -> ML_Pretty.pretty |
77 val to_ML: FixedInt.int -> T -> ML_Pretty.pretty |
78 val from_ML: ML_Pretty.pretty -> T |
78 val from_ML: ML_Pretty.pretty -> T |
79 val to_polyml: T -> PolyML_Pretty.pretty |
79 val to_polyml: T -> PolyML.pretty |
80 val from_polyml: PolyML_Pretty.pretty -> T |
80 val from_polyml: PolyML.pretty -> T |
81 end; |
81 end; |
82 |
82 |
83 structure Pretty: PRETTY = |
83 structure Pretty: PRETTY = |
84 struct |
84 struct |
85 |
85 |