pp.all true regression

Stream: general

[Kevin Buzzard]

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]

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]

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