40d6a6def0
The formatter was using `tk ++ " "` to separate tokens from tokens they would merge with, but `" "` is not whitespace that could merge. This affected large binder lists, which wouldn't pretty print with any line breaks. Now they can be flowed across multiple lines. Closes #5424 |
||
|---|---|---|
| .. | ||
| Delaborator | ||
| Basic.lean | ||
| Delaborator.lean | ||
| Formatter.lean | ||
| Parenthesizer.lean | ||