Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #614. Cause by 8215623. #615

Merged
merged 1 commit into from
Nov 9, 2021
Merged

Conversation

Matafou
Copy link
Contributor

@Matafou Matafou commented Oct 22, 2021

The regexp change in 8215623 to support "Fail" command had to be
refined to capture correctly some error messages.

The regexp change in 8215623 to support "Fail" command had to be
refined to capture correctly some error messages.
@Matafou
Copy link
Contributor Author

Matafou commented Oct 25, 2021

This fix is a bit fragile but we need to fix error highlighting quickly. So I will merge this soon.

For the record and a future better implementation:

The fragility comes from the fact that the <P>-error-regexp is used in two ways: either on the string <PA>-last-output or directly in the response buffer with re-search-forward. I think it would be cleaner if used only on the string.

Once it is only done on the string, we could have an optional <PA>-match-error-p function which would take precedence over <PA>-error-regexp taking a string and testing if it contains an error message. It would allow for a better fix for #597, avoiding negative regexp.

No hurry though.

@Matafou
Copy link
Contributor Author

Matafou commented Nov 9, 2021

The bug #612 has nothing to do with this PR. I merge.

@Matafou Matafou merged commit 2145c23 into ProofGeneral:master Nov 9, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant