Thanks. Agreed. On Wednesday, February 9, 2022 at 2:16:41 PM UTC+1 [email protected] wrote:
> 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/bcc58547-ace7-40f3-9257-362cb0f6fa48n%40googlegroups.com.
