feat: include `ppLine` in `many(1)Indent`

[tydeu]

I noticed many1Ident did not pretty print lines during this Zulip thread. Including ppLine within manyIdent will help end users get better pretty printer output without needing initmate knowledge of when to use the pp* helpers.

[digama0]

It would be best to test this against mathport to make sure there are no unforeseen issues.

[tydeu]

@Kha Does this need a stage0 update or similar for the change to many(1)Indent to appear in the tests? Or is this an actual bug on my end?

[tydeu]

@digama0 What is the best way to do that? For instance, after building mathport with the custom Lean, what should I port?

P.S. Also, since you are here and you have experience with this kind of stuff, does this need a stage0 update for the manyIndent change to appear in the tests?

[digama0]

A change to indentation should not require a stage0 update, since it doesn't affect the actual semantics of the parsers. AFAIK they should just work in the tests (that use stage1 for testing).

For testing mathport, you will need to at least create a toolchain build for this PR, and then I can point mathport to it in a mathport draft PR or similar.

Looking at the test failures, it appears there are already some undesirable formatting changes which need to be tweaked. I don't think there are any build issues here, you just changed the formatting and will have to update any test .expected files when the change is good and fix the code when the change is bad.

[tydeu]

@digama0

Looking at the test failures, it appears there are already some undesirable formatting changes which need to be tweaked. I don't think there are any build issues here, you just changed the formatting and will have to update any test .expected files when the change is good and fix the code when the change is bad.

In that case, there is probably a bug. There should be no changed in formatting. All the parsers which used many(1)Indent thus far already had a ppLine, so moving it into manyIndent should not have changed the formatting at all (unless there is something I am missing).

[Kha]

Indeed that looks buggy. I didn't take a closer look than that.