In particular, the head comment (you know, the one that takes up the first 1/5 of the file) is one such comment, and rewrapping this comment would destroy the changelog.
On Wed, Feb 9, 2022 at 8:14 AM Mario Carneiro <[email protected]> wrote: > It's almost certainly the latter. Markup validation also only works on > comments before a $a/$p statement, so I imagine using the markup-aware > rewrapper on a comment that could contain arbitrary unvalidated text could > do significant formatting damage. > > On Wed, Feb 9, 2022 at 7:44 AM Benoit <[email protected]> wrote: > >> I just noticed that apparently, rewraps are not done within double quotes >> either ? For instance, set.mm contains: >> $( Major premise for the Aristotelian syllogism "Barbara", e.g., >> "All men are mortal". By convention, the major premise is first. $) >> >> Note that the first line could be longer (rewrap could be after "men"). >> Also, the single space after 'mortal".' should be a double space. Or is it >> because this comment is not right before an assertion ($a or $p statement), >> and only these comments are reformatted/rewrapped ? If so, then shoud >> reformat/rewrap be extend to all comments, for more consistency ? >> >> Benoît >> >> >> >> >> >> On Tuesday, February 8, 2022 at 5:57:39 AM UTC+1 Alexander van der Vekens >> wrote: >> >>> On Tuesday, February 8, 2022 at 3:45:30 AM UTC+1 [email protected] wrote: >>> >>>> I was considering it. Or at least, deprecating it once we have an >>>> adequate replacement, which can then have a different behavior on long math >>>> strings. >>>> >>>> If we're keeping the current behavior, I suppose that means that there >>>> should be a warning for newlines in a math string? >>>> >>> >>> To get a warning in this case would be great! >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/537e395a-b398-486c-a4c6-bdb8a0f0f23an%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/537e395a-b398-486c-a4c6-bdb8a0f0f23an%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsmjeE9g%2BWw4-GtjCkU1%3Dcs58CZudFj3YV43i0SrhDqEQ%40mail.gmail.com.
