There is another matter that I can't seem to find any discussion about: Math markup strings in set.mm are exclusively single-line, even going to the extent of closing the string and reopening it on the next line if needed to wrap a line. But I can't find any evidence in metamath.exe of this behavior: VERIFY MARKUP doesn't care if you have newlines in a math string, and it displays just as you would expect. Maybe this is /REWRAP 's doing? Should the new markup checker enforce that math strings have no newlines, or allow them? Personally I don't see any reason other than historical momentum to disallow newlines in math strings.
On Fri, Feb 4, 2022 at 6:15 AM Mázsa Péter <[email protected]> wrote: > ok, I'll fix this after #2472 merge > > On 2/4/22, Mario Carneiro <[email protected]> wrote: > > FYI, I made some minor stylistic modifications to the el*v theorems in > > https://github.com/metamath/set.mm/pull/2472 ; you should use that as a > > base for modification to avoid conflicts. > > > > On Fri, Feb 4, 2022 at 4:35 AM Mázsa Péter <[email protected]> wrote: > > > >> On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > >> > * I agree with Mario that stars should not be allowed after or within > >> > labels, at least if they are used with ~ to auto-link them. > >> > >> Of course I agree as well. 4 options remained: > >> ( ~ elv , and the theorems beginning with ` el2v ` or ` el3v ` ) > >> ( ~ elv , and the theorems beginning with el2v or el3v ) > >> ( ~ elv , ` el2v* ` and ` el3v* ` theorems) > >> ( ~ elv , el2v* and el3v* theorems) > >> Perhaps the first is the best, I'll make experiments. > >> > >> On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > >> > Wouldn't $p ` |- ( A e. V -> ` be sufficient? > >> On 2/3/22, Mario Carneiro <[email protected]> wrote: > >> > For the purpose of > >> > this particular comment I think it suffices to just have ` |- A e. _V > ` > >> in > >> > the description. > >> > >> I agree here as well, I will try this: > >> Inference forms (with ` |- A e. _V ` ) of the general theorems (with ` > >> |- ( A e. V -> ` ) may be superfluous. > >> > >> On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > >> > * quoted strings longer than a line can be split up. See, for example, > >> > ~ > >> > numclwwlk7. I think this is a sufficiently good solution. > >> On 2/3/22, Mario Carneiro <[email protected]> wrote: > >> > As mentioned, the fix is to split the math string by closing it on the > >> > first line and reopening it on the second line. The renderer will > >> > combine > >> > the strings. > >> > >> This is perfect! I didn't know about this option. Thank you. > >> > >> > >> Peter > >> > >> -- > >> 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/CAJJTU5ppfdp40ZM9suURAKNc%2BDNqJnZubhzVsFudGQwdTa1uaw%40mail.gmail.com > >> . > >> > > > > -- > > 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/CAFXXJSutsO728YztaxsAhYeuyR%2BVnRop2f4yzpWR7uTcF%2BtaYg%40mail.gmail.com > . > > > > -- > 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/CAJJTU5rjfouTa4z6jv4BA81gnabkfVDz_8HGNCUua_x_JTugbw%40mail.gmail.com > . > -- 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/CAFXXJStFmRok27b%2BtQNLN2X0bkipOcHxidHDveWyMTYtfTsgpA%40mail.gmail.com.
