Report line numbers associated with (non-parsing) HOL_ERRs

[mn200]

When parsing fails, it gives back useful numbers because the quotation filter puts line numbers into the quotation strings that are being parsed. Under Poly/ML, it might be possible to

1. embed the quotation filter into the interactive loop
2. have the quotation filter update some sort of global resource so that tactics etc are associated with line numbers, and these can then be reported when the function fails

This may be completely impossible

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.