I want to do ast parsing. However, it's possible that my code have some error to let the proof not able to continue. In that case, I still want to parse. It seems that Lean Repl haven't implemented this?
See discussion in
augustepoiroux/LeanInteract#24