equal
deleted
inserted
replaced
64 | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); |
64 | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); |
65 |
65 |
66 fun pretty_rule (lhs, rhs) = |
66 fun pretty_rule (lhs, rhs) = |
67 Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; |
67 Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; |
68 |
68 |
69 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast); |
69 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast); |
70 |
70 |
71 |
71 |
72 (* strip_positions *) |
72 (* strip_positions *) |
73 |
73 |
74 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) = |
74 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) = |