ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

PG does not position to error of vernacular commands #790

Open hendriktews opened 1 month ago

hendriktews commented 1 month ago

When I process a buffer just containing

Comput x.

I get error in process filter: End of buffer, because PG tries to move point to an illegal position. With some non-empty lines below Comput, PG puts point to a wrong location. With just newlines below Comput, I get some other error.

Same for Require xxx., where Require is valid, but module xxx does not exist.

When I switch back to 0e0170f96f5feaeefe59052a08373080acc20393, before #774 error positioning does work fine.