## Stream: general

### Topic: pp.all true regression

#### Kevin Buzzard (Jul 11 2020 at 21:44):

set_option pp.all true used to print out terms with really nice whitespace, making them about as readable as one can hope. Now with the widgets I just get a stream of @blah's; it's much harder to read.

Example:

⊢ @eq.{1} G (@has_mul.mul.{0} G (@has_mul.mk.{0} G (@lftcm.group.mul G _inst_1)) (@has_inv.inv.{0} G (@lftcm.group.to_has_inv G _inst_1) a) (@has_mul.mul.{0} G (@has_mul.mk.{0} G (@lftcm.group.mul G _inst_1)) a b)) (@has_mul.mul.{0} G (@lftcm.monoid.to_has_mul G (@lftcm.group.to_monoid G _inst_1)) (@has_inv.inv.{0} G (@lftcm.group.to_has_inv G _inst_1) a) (@has_mul.mul.{0} G (@lftcm.monoid.to_has_mul G (@lftcm.group.to_monoid G _inst_1)) a b))


Before, it would have been much clearer what the fully expanded terms on each side of the equality were.

#### Scott Morrison (Jul 23 2020 at 06:24):

Even for none pp.all mode, for any non-trivial goal the current goal display is unreadable. Is anyone able to look into restoring proper indenting for multiline goals? I'm working in plain text mode today. :-(

#### Kevin Buzzard (Jul 23 2020 at 06:52):

Oh yes when j wrote that I didn't know you could switch back!

Last updated: May 08 2021 at 09:11 UTC