I just noticed when rereading the metamath code for https://github.com/metamath/metamath-exe/pull/90 another behavior I haven't captured yet in the metamath-knife parser: In typesetting comments, you can use "foo" or 'bar' quoted strings as tokens, and these do not accept any escapes. *However*, it turns out that "a""b" does count as a single string (it must be two quotes in a row - "a" "a" is two tokens but "a""a" or 'a''a' is one string token). But counter to intuition, "a""a" is actually a string which contains two double quotes, i.e. <a""a>, and similarly 'a''a' encodes <a''a>. At least, this is the behavior I observed when trying this out in althtmldef, I didn't try all the commands to see if they act the same way.
This seems like such an obviously useless and incorrect behavior that I am inclined not to replicate it in metamath-knife. What do people think? The current metamath-knife behavior is to not allow any internal quotes in the string, so "a""a" is two adjacent string tokens. On Wed, Feb 9, 2022 at 8:28 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/bcc58547-ace7-40f3-9257-362cb0f6fa48n%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/CAFXXJSsfzvsU-cj2n-hYfwcTESNztvqegZ9jf97fowpAWsoCDQ%40mail.gmail.com.
