search

PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
136 stars 23 forks source link

Emit errors if labels could not be resolved #3

Closed zeramorphic closed 7 months ago

zeramorphic commented 2 years ago

If labels have no referent, emit a plasTeX error instead of simply ignoring the label. Users can, of course, simply ignore this error - it doesn't cause the compilation to stop. This is primarily of interest when refactoring large blueprints, as names of labels are changed frequently. This change has already revealed a few incorrect labels in the con-nf project.

PatrickMassot commented 7 months ago

Thanks. I'm sorry I didn't see this PR earlier.