Oops, this is actually a bug, the very same bug that #90 is fixing. The doubled quote is supposed to be undoubled when interpreted, so "a""a" means <a"a> and 'a''a' means <a'a>, which seems like a lot more reasonable behavior. It still seems unnecessary though; is it worth supporting?
On Thu, Jun 9, 2022 at 2:05 PM Mario Carneiro <[email protected]> wrote: > 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/CAFXXJSvAjVRCv%2B1Xt7_DvNmADkNOZgxzMghrDnP%2B8kc_GM-zGg%40mail.gmail.com.
