I added support for it in https://github.com/david-a-wheeler/metamath-knife/pull/91 . You can already obtain strings like <a'a> by using the other quote character - "a'a" - and if you need both ' and " you can sometimes use + to concatenate strings, e.g.
htmldef "foo" as "[']" + '["]'; would render foo as the string <[']["]>. However this + concatenation trick is not general purpose in $t comments, it is tokenized as a bunch of string literals and + keywords and it is up to the command to support this or not. Most of the $t commands support it but only in the second argument (after the "as"), and none of the $j commands support it. There isn't much demand for it in the other places though; it's not needed if you are only listing statement labels since these are not long enough to need line breaks and don't use quote characters anyway. On Thu, Jun 9, 2022 at 8:55 PM Benoit <[email protected]> wrote: > If you do not support this, then is there another way to obtain the > strings <a'a> and <a"a> ? > > On Thursday, June 9, 2022 at 8:14:16 PM UTC+2 [email protected] wrote: > >> 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/5399ef9b-ae28-435b-adbb-3a6159f71458n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/5399ef9b-ae28-435b-adbb-3a6159f71458n%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/CAFXXJSv%2BQMs6VFd8FfEnAF72JLLwnBa1_7RQEEVdqwXON3FNbQ%40mail.gmail.com.
