Clarify rules about $t

[david-a-wheeler]

(This is split from issue #15).

Norm Megill wanted to clarify the rules for $t; here is my reply:

(1) My to-do note was intended to address whether $t needs to be surrounded by whitespace (I would recommend yes, for simplicity).

That would require rewriting all the $t statements, and current code already handles it. Personally I'd leave it be, but it's up to you.

(2) Also, it isn't clear whether anything other than whitespace can go between the start of the comment and the $t (I would recommend no, for simplicity). In the current metamath.exe, I believe that neither of these cases are currently enforced, but I can add code to 'verify markup' to enforce them.

I like that idea (idea 2), and set.mm already meets that criteria.

Should I try to add at least "only whitespace before $t rule (idea 2) to the text?

[nmegill]

(1) My to-do note was intended to address whether $t needs to be surrounded by whitespace (I would recommend yes, for simplicity).

That would require rewriting all the $t statements, and current code already handles it. Personally I'd leave it be, but it's up to you.

I didn't mean the content of the $t comment, just the $t token itself. All current .mm files (I checked set.mm, iset.mm, nf.mm, hol.mm, ql.mm) have the $t surrounded by whitespace. The rest of the $t comment contents will continue to have their somewhat liberal whitespace rules.

Perhaps it is silly to single out the token "$t" for requiring surrounding whitespace, and I'm fine with leaving the spec alone in that regard.

[david-a-wheeler]

Ah, okay. How about this:

There must be 1 or more white space characters, and only white space characters, between the $( and $t, and the $t must be followed by by 1 or more white space characters.

I think that's a reasonable clarification.

[david-a-wheeler]

Also: I think we should document that currently only one $t is supported in the Metamath program, but say that constraint may be lifted in the future.

If we split things into files, it'd make more sense to have $t settings for that file in the file. It might even make more sense to have $t statements next to the symbol they declare. The set.mm database might never do that, but others might want to.

[nmegill]

That is fine. I will add a to-do item on my list to have the 'verify markup' command check this.

[nmegill]

Also: I think we should document that currently only one $t is supported in the Metamath program, but say that constraint may be lifted in the future.

If we split things into files, it'd make more sense to have $t settings for that file in the file. It might even make more sense to have $t statements next to the symbol they declare. The set.mm database might never do that, but others might want to.

I agree. Off and on I have thought about splitting up the $t, say one $t per mathbox or even per $c, but each time I've ended up deciding it's more convenient to have them all in one place, especially when making global changes to the list such as the change to XITS fonts. So I haven't yet been sufficiently motivated to add the code to split them up. But it is a future possibility, and I have a to-do item to look into it eventually.

[david-a-wheeler]

Very good. I think this issue is completely resolved, so I'm closing it.