After playing with rewrap a bit, I think the reason for the restriction is that "write source /rewrap" will not attempt to break math strings, but it will remove newlines from math strings, meaning that if you have a long math string containing newlines it will be rewrapped into a long line, which then fails to pass verify markup.
This leaves the question of what to do, however. The rewrap command could reflow math tokens, but this almost always looks terrible, which is why it doesn't do this for regular statements unless they go over the line limit. A more reasonable approach would be to preserve any internal whitespace in a math string, to allow for manual indentation. On Mon, Feb 7, 2022 at 4:06 AM Mario Carneiro <[email protected]> wrote: > 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/CAFXXJSs213mdiSJsSp1VdtnTY9RST9cvPKAVyT18QosfgwhPNw%40mail.gmail.com.
