search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

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

Open MostAwesomeDude opened 10 months ago

MostAwesomeDude commented 10 months ago

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 commented 10 months ago

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 commented 10 months ago

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