changeset 25430 | 372d6749f00e |
parent 23510 | 4521fead5609 |
--- a/src/Tools/Metis/src/Parser.sml Tue Nov 13 17:04:16 2007 +0100 +++ b/src/Tools/Metis/src/Parser.sml Tue Nov 13 18:29:28 2007 +0100 @@ -129,6 +129,7 @@ fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppTrinop "," "," ppA ppB ppC); +(* Keep eta expanded to evaluate lineLength when supplied with a *) fun toString ppA a = PP.pp_to_string (!lineLength) ppA a; fun fromString toS = ppMap toS ppString;