[cvs-nhc98] patch applied (hat): Replaced the old ugly and inefficient pretty printer by a new efficient one.