332 bug lean starting subproof gives scary warning

[GitLuckier]

From the vscode side, we now receive the hideFromBottomPanel diagnostic message. This is to prevent messages like unsolved goals in a subproof from scaring the user by not showing them below an input panel.

To test this PR, checkout branch 332-bug-lean-starting-a-subproof-gives-a-scary-warning in impermeable/waterproof-vscode. Start a subproof by using a \. character. The error message should no longer appear on the bottom of the input area (only if the unsolved goals is inside the input area). Other error messages should be uneffected.

This is done to resolve impermeable/waterproof-vscode#332. However, I am not quite satisfied with the result, because it also hides the red squiggly line that would normally appear below the subproof dot. This squiggle shows the user that the subproof has not been solved yet. From the issue description, it wasn't really clear to me what the desired end result was. If desired, I can also show a shorter error message instead of the whole thing. However, if we want to HIDE the error message AND still show the squiggle, the best way (without any hacks) would be to ask the CodeMirror maintainer Marijn if we could do this using the linter. Currently, you can say whether you want the error to show a tooltip, but you cannot prevent it from showing up in the bottom panel (trust me, I tried).

If the current approach is already sufficient and does not need to red squiggle, then please go ahead and merge this.

[pimotte]

Is there a way we can spawn the error on the QED instead? It doesn't have to be the full/same error as otherwise, but this is what happens when you've normally not finished a proof. Then we're also not showing the full error in the editor, because we only do this in code cells contained in input areas.