shorten ifpfal #1695
shorten ifpfal #1695
Conversation
Hmm. This shouldn't happen, although no one has reported it before. I confirmed what you are seeing, and it looks like a bug. I will fix it, hopefully in the next release of metamath.exe. Thanks for reporting it. |
It turns out that I did this intentionally (a long time ago) to ensure that all comments, including those with "<HTML>", had consistent indentation. As you point out, this makes it impossible to have local indentation in the comment itself. In version 0.183 (30-Jun-2020) of metamath.exe that I just updated, I took out the indentation adjustment for comments containing "<HTML>", so these comments are now not touched at all anymore by "/rewrap". You can use any indentation you want. Even if you start them in column 1 it will not complain or make any adjustments. This means some more manual effort will be needed to keep the formatting tidy, but I think it is a small price to pay for the extra flexibility. Some notes about the "<HTML>" tag: (1) it is case sensitive; (2) if it occurs anywhere in the comment, the whole comment is treated as HTML; (3) additional occurrences of "<HTML>" are ignored (and all occurrences are discarded before generating the web page); (4) the tag "</HTML>" is deprecated, and any occurrences are ignored and discarded before generating the web page; (5) the only difference in the generated web page when "<HTML>" is present is that "<" and ">" are not translated to "<" and ">". BTW "&" is not converted to "&" in either <HTML> or non-<HTML> comments, so that Unicode entities can be used in either kind of comment. Note that a comment cannot be broken up into HTML and non-HTML sections using "<HTML>...</HTML>" as those tags suggest. Either the comment is all HTML or none of it is. Although multiple occurrences of "<HTML>" and any occurrences of "</HTML>" are currently tolerated, in the future I may have them produce "verify markup" warnings. Some existing comments will then have to be adjusted to remove them. As a convention, I suggest that "<HTML>" be placed at the beginning of a comment that needs it. For the long term, I have been considering removing the "<", ">" translation to "<", ">" from any comment (i.e. we make HTML the comment language), so that the only effect of "<HTML>" would simply be to prevent wrapping by "/rewrap". In that case, the "<HTML>" tag could be renamed to something more meaningful like "<NOWRAP>". |
|
Thanks for caring about that. I think the contents of your last comment should be made available in a less hidden place. Wolf |
The block of HTML list items
< li> a : theorem having a conjunction as antecedent< /li>
...
were unindented by rewrap, which in my eyes decreases the readability of the HTML code. Despite this I accepted the downgrade to further support automatic uses of rewrap.