Zulip Chat Archive

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.


 @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: Aug 03 2023 at 10:10 UTC