equal
deleted
inserted
replaced
4 Extra toplevel pretty-printing for Poly/ML 5.3.0. |
4 Extra toplevel pretty-printing for Poly/ML 5.3.0. |
5 *) |
5 *) |
6 |
6 |
7 PolyML.addPrettyPrinter (fn depth => fn _ => fn str => |
7 PolyML.addPrettyPrinter (fn depth => fn _ => fn str => |
8 ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); |
8 ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); |
|
9 |
|
10 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => |
|
11 ml_pretty (Pretty.to_ML (XML.pretty depth tree))); |
9 |
12 |
10 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
13 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
11 pretty (Synchronized.value var, depth)); |
14 pretty (Synchronized.value var, depth)); |
12 |
15 |
13 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
16 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |