Sorry is invalid, hint is incorrect, isBusy flag properly resets.

[GitLuckier]

Description

sorry and hint were marking the input areas as Correct. This should fix it. sorry is now marked as Invalid. The This pull request also fixes an issue where theisBusy` flag would sometimes not properly reset.

Changes

When a user types sorry, Lean will not mark the input as using sorry, but will mark the theorem. This means that the message "deceleration uses sorry" will appear outside the input area. In order to link the input area with this message, we look if there are any sorry messages between the end of the current input area and the end of the previous one. Then we mark that input area as invalid. Same for hint, since it also sends sorry messages when used.

I also removed a mistake I made with the isBusy flag being set with this function called onDocumentChanged. This function shouldn't be in there any more, so I removed it. This fixes a bug where correct input area fields would stay permanently red, because isBusy wasn't being set to false.

renamed client.determineProofStatus.test.ts to client.proofStatus.test.ts to be more inclusive of functions other than determineProofStatus.

Testing this PR

• Open your favourite Lean document.
• Type sorry or hint.
• Observe that only the input area you selected is turning yellow
• Input areas that are correct should no longer stay red forever when typing in other input fields. (isBusy)

There are also a few automated unit tests. Most notably, this approach requires getInputAreas to return a sorted array, I have written tests to ensure that this is always the case

Closes #328