And here my remarks on Mario's rules/checks:
> - * 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. > > This is OK as strict rule and fits to the conventions we have already documented in set.mm (space-separated tilde) - * Space *before* ~ seems to have a lot of violators, so unless we like the look of it I'm okay with relaxing this restriction. This would also fit to the conventions we have already documented in set.mm (space-separated tilde). I would propose to clean up set.mm and make it a strict rule. - * 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. This rule should be kept (and checked). - * 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. I think such a rule would be too restrictive, and we should not enforce 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. There ARE real URLs which contain ~. In such URLs, ~~ must be used, see mmset.raw.html "http://www.math.miami.edu/~~ec/book";. What exactly happens if this is written as "http://www.math.miami.edu/~ec/book";? - * 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. As far as I can remember there are strict rules for bibliographic references (no whitespaces, etc.) , and all other cases are interpreted literally. We should stick with this and should not enforce the usage of [[ in these cases. - * 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). I cannot really imagine such a case, but to reject such constructs sounds fine. - * In bibliography references, there are no escapes but ~ and ` break metamath.exe, so there are no violators. I do not really understand this case. Could you give an example? - 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. Really funny, but this won't be possible in the future (if the strict space-separated tilde rule is enforced): it will have to be either "~ [ab]", then [ab] must be a label, or "~~[ab]", then [ab] must be 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. If this can be checked, it should not be allowed in the future. > -- 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/0f9f9859-88d7-4738-8ef1-a8dd50cbd995n%40googlegroups.com.
