Formatting bug

[benjub]

As noticed in metamath/set.mm#2689 (comment), it looks like in some cases (but not all) when a $p-statement is written with $p ending a line (hence the next line begins with |-), then the proof is not indented (see currently ~eucalg in set.mm, but notice that e.g. ~stirlinglem5's proof is correctly indented).

[savask]

I think I found the root of the bug. Here's a small example:

  $c A $.
  $( An axiom. $)
  a1 $a A $.
  ${
    $( A theorem.  (Contributed by XX, 01-01-1970.) $)
    th $p
      A $= ( a1 ) A $.
  $}

After save proof */compressed/fast and write source ... /rewrap we get

  $c A $.
  $( An axiom. $)
  a1 $a A $.
  ${
    $( A theorem.  (Contributed by XX, 01-01-1970.) $)
    th $p
      A $=
  ( a1 ) A $.
  $}

The problem seems to be in the getSourceIndentation function of the file mmdata.c. It is used to compute indentation for the proof block, so when it's called in our example the fbPtr pointer points at a newline right after $p token, and this immediately stops the while(1) loop computing indentation.

It seems that the fix is too add the line

  if (fbPtr[0] == '\n') fbPtr--;

right before the while loop. I ran the version of metamath with the fix on set.mm, and the only affected lines are the ones with proofs with broken indentation, so it seems that the fix doesn't do any harm. Formatting is a delicate subject, so I would be glad to hear opinions of other metamath-exe contributors (maybe @digama0 or @wlammen can take a look?).

[wlammen]

I think one can unconditionally step back one character, so you are on the p of the $p (if this is the keyword), no matter what character is following
The comment /* Go back to first line feed prior to the label */ is misleading. The first line feed (LF) before the keyword determines the indentation. In theory the label and keyword may be separated by one or more LF.

[benjub]

@wlammen or @savask : can you make a PR with the fix you proposed ?

[wlammen]

I am not going to add a PR on my behalf, before #100 is finished, and that project seems to have ground to a standstill already at the second step.

[savask]

@benjub I have my another PR stuck in the queue (about minimization), so I'll wait till it is resolved.

[benjub]

@savask I think there would be no merge conflicts between the two PRs. I whish I could help (and also for @wlammen's #101) but my C skills are not up to the task. I can understand what your patch in #94 does but cannot certify it is bug-free :(