search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

Nested Includes Bugfix #47

Closed ml-2 closed 3 years ago

ml-2 commented 3 years ago

I used the split mechanism explained in this issue of set.mm: https://github.com/metamath/set.mm/issues/1741#issuecomment-667720659

However, when splitting set.mm there are nested include statements, and a bug in mmj2 gives errors such as this:

E-LA-0008 Inactive (in scope) symbol used in statement expression. Symbol = A Source Id: set-deprec.mm Line: 8940 Column: 37
E-LA-0007 Undefined symbol used in statement expression. Symbol = U Source Id: set-deprec.mm Line: 8941 Column: 37
E-LA-0007 Undefined symbol used in statement expression. Symbol = W Source Id: set-deprec.mm Line: 8942 Column: 34
E-LA-0007 Undefined symbol used in statement expression. Symbol = Fun Source Id: set-deprec.mm Line: 8950 Column: 68
E-LA-0008 Inactive (in scope) symbol used in statement expression. Symbol = A Source Id: set-deprec.mm Line: 8954 Column: 36
E-LA-0007 Undefined symbol used in statement expression. Symbol = U Source Id: set-deprec.mm Line: 8962 Column: 19
E-LA-0019 Variable = P in statement not previously declared. Source Id: set-deprec.mm Line: 8966 Column: 13
E-LA-0019 Variable = Q in statement not previously declared. Source Id: set-deprec.mm Line: 8966 Column: 24

This pull request is a small fix for that bug, as well as a recompiled mmj2.jar containing the fix.