FStar
FStar copied to clipboard
Send response when lookup IDE request fails.
The lookup request is the only one which does not return any response if the request failed. This makes it hard to support it in a generic API for IDE requests. See discussion at https://github.com/FStarLang/fstar-vscode-assistant/issues/27#issuecomment-1889687807
The history of the failure response for this request is interesting: it has flipped several times over the last year. I have summarized the responses for the different editors in the table below. I could not find any justification for the changes, the current vscode extension seems to work just fine with the change. This PR effectively reverts the behavior to how it was in 2022.
| time | vscode | emacs |
|---|---|---|
| 2022 | NOK | NOK |
| after 754a6d8f1d2d5c6a0816bf24499a12896e0eb369 | OK | OK |
| after 6f979fb1dd53ada793682bd892473e78225fe05a | nothing | NOK |
| after this PR | NOK | NOK |
So apparently the lookup query is used internally by full-buffer.
So apparently the
lookupquery is used internally byfull-buffer.
I've added a new internal query type to ignore errors. The full-buffer command now uses this to suppress error messages when generating the internal lookup queries, while keeping the 2022 semantics of lookup. (Though I don't think the error messages broke anything except for the tests.)
The vscode extension now avoids the awkward version of the lookup query, and no longer uses the internal lookup queries either.
The right choice is probably to just remove the internal lookup queries entirely.