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.
