Tesla Zhang‮

> Btw how does Arend solve this? Their JB plugin uses a different parser which is fault-tolerant (JB has a general framework for code completion).

> Can we have some fault-tolerant parser? Idk if you could reuse GK

> It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html Is that easy to adapt in Aya?

@re-xyr It doesn't have a good Java rewrite/binding yet. JetBrains has a JNI-based binding, but I ain't sure if it's open sourced or "good" in any sense.

> > > It seems ANTLR4 can recover: https://www.antlr.org/api/Java/org/antlr/v4/runtime/ANTLRErrorStrategy.html > > > > > > Is that easy to adapt in Aya? > > It's a little difficult. ANTLR does...

 Quite easy.

 Maybe we can just look at the default implementation

 This is what I see. They're heavily documented

@re-xyr I have no idea. Probably we should only implement file-level incremental compilation as Agda to avoid the complications

/cc @ShreckYe