By default don't use discouraged syntax nor later syntax

[david-a-wheeler]

Currently a2i is being syntactically parsed in an unexpected way. Its final statement is:

( ( ph -> ps ) -> ( ph -> ch ) )

As you showed in your video, clicking on the first -> unexpectedly selects the whole phrase instead of just ( ph -> ps ). That's because metamath-lamp ends up using the discouraged syntax statement bj-0.

I think that's a problem, the question is how to correct it. I think this is fine for v11 but does need correcting long-term.

I think discouraged syntax should be ignored by default in the editor (controlled by settings) unless there is literally no other way to parse something. If that's too hard, I'd just say "ignored by default in the editor" (controlled by setting), because that will handle the vast majority of cases without change. I believe discouraged syntax is REALLY unusual, even more unusual than discouraged theorems or axioms. Allowing the use of discouraged syntax should probably require a separate checkbox that 99% of users would ignore and just leave at "do not use discouraged syntax".

In addition, in the explorer or separate tabs, no statement should be able to use syntax assertions after their position in the database (no matter what). Basically, respect their context. That would prevent problems copying from those assertions.

[expln]

I think the proposed solution will work. The part unless there is literally no other way to parse something is indeed hard to implement. Individual tabs already respect their context. Everything else is not too difficult to implement. Thanks for documenting this as an issue.

[david-a-wheeler]

Great! BTW, please do make it possible to use discouraged axioms or theorems while not using discouraged syntax. I've used a number of discouraged axioms and theorems, in fact, we want people to do that sometimes because it's our information hiding mechanism. I have never intentionally created nor used discouraged syntax :-). The other tools hide it, but your really cool fragment selector reveals it. Best to reveal what we want them to use :-).

[expln]

please do make it possible to use discouraged axioms or theorems while not using discouraged syntax.

This is implemented on dev. Please read this comment to understand how this works.

[david-a-wheeler]

This is great! Thanks so much! This will make the syntax highlighting "work as expected" for most users, as well as producing the "expected proofs".

Many years ago mmj2 allowed discouraged theorems in proofs, and we were constantly replacing the discouraged theorems with the "expected" theorems. It was an unnecessary speed bump for new people. Fixing it here will be even more valuable, because mmj2 doesn't have anything like metamath-lamp's syntax-aware highlighting.