... I suppose it's apropos that a post about bugs in text->html autoformatting would itself have buggy formatting. Please ignore the non-ascii list item formatting.
On Wed, Feb 2, 2022 at 9:39 PM Mario Carneiro <[email protected]> wrote: > Hi All, > > I've been working on a reimplementation of metamath.exe's VERIFY MARKUP > feature for metamath-knife, you can see the highlights at > https://github.com/david-a-wheeler/metamath-knife/pull/70 . It's already > started catching some bugs that will be PR'd to set.mm once the checker > stabilizes, but I wanted to bring specific attention to two rules which > have produced hundreds of new errors on set.mm: > > > - 23. The ~ and ` characters, when used as delimiters in markup, > should have whitespace around them > - 24. Characters [, ~ and ` must be doubled if they could not be > interpreted as special in markup > > - Some of the violators have been highlighted at > > https://github.com/david-a-wheeler/metamath-knife/pull/70#issuecomment-1027601499 > . > - > - The question is: Should these rules be kept? > > * The use of space after ~ was used to make it easier to find labels > in comments for find/replace activities, and I think there are only a small > handful of violators. > - * Space *before* ~ seems to have a lot of violators, so unless we > like the look of it I'm okay with relaxing this restriction. > - * Space after the initial ` and before the final ` in a math string > has no violators at a glance, I think VERIFY MARKUP was already checking > this. > * Space before the initial ` and after the final ` in a math string > has lots of violators for things like (` e. `). Metamath will strip the > surrounding spaces if it is a closing punctuation, but there are also > examples like "I` /\ `2" in the description of natural deduction rules > where the added spaces would be preserved, which is undesirable in this > case (we want it to read I∧2). Using unicode html entities would be an > alternative way to handle this. > - * Non-doubled ~ inside a URL was already being warned against in > metamath.exe, although arguably it's fine since it doesn't do anything and > is interpreted literally. > - * Non-doubled [ has lots of violators in set.mm. There are examples > that seem to suggest that people are relying on [ getting printed literally > as long as the ] comes after a space. Something like [foo] has to be > written as [[foo] because otherwise it would be interpreted as a > bibliography tag, but [foo bar] can't be a tag and is interpreted > literally; this is the case that triggers the new warning. > - * In label/url mode, non-doubled ~ is already warned by metamath.exe > and there are no violators, but non-doubled [ interacts weirdly with > bibliography tags, and I think rejecting these is the right thing to do > (there are no violators). > - * In bibliography references, there are no escapes but ~ and ` break > metamath.exe, so there are no violators. > > - Some more fun things: > * ~[ab] gets interpreted as *both* a bibliography tag and a label > reference, resulting in a broken link to the statement [ and a link to the > bibliography tag "ab". Currently mm-knife does the next best thing which is > to interpret it as an empty label reference followed by a bibliography tag. > - * ` alone in a comment starts math mode and doesn't end it, so you > get a warning about "</TD></TR></TABLE></CENTER>" not having an html > definition. Naturally, you can therefore add a token called > </TD></TR></TABLE></CENTER> and give it htmldefs and it will pass VERIFY > MARKUP, and the resulting HTML file will look just a bit off. > > -- 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/CAFXXJStewJedDRcyp_GnCH2NO4zSX4A__eKMF620a%3DvdAA56kg%40mail.gmail.com.
