Only one typesetting comment ($t) is allowed per database

[MostAwesomeDude]

Quoting the PDF, p144:

In version 0.177 of the Metamath program, there may be only one $t comment in a database. This restriction may be lifted in the future to allow many $t comments in a database.

I would like to lift this restriction.

I am generating part of a database from structured data. I've arranged my generated data so that it can be appended to the end of an existing database. My generated data includes labels which are not in the main database, and I'd like to generate a typesetting comment ($t) so that those labels can be correctly formatted.

I'm planning on working around this for now, since my build step allows for aggressive sed incantations, but I'd prefer if I were able to merely have multiple $t which are monoidally aggregated.

[digama0]

Agreed, this is a silly restriction which is not present for $j comments (which are otherwise identical parsing-wise) and necessitates some very inconvenient separation of typesetting info from constant declarations.

[tirix]

Agreed - the code to change appears to be in mmwtex.c, in the readTexDefs function.