feat: added diagnostics converter patch

[GitLuckier]

Changes

The Lean LSP inlcudes non-standard fields inside their diagnostic messages. These properties get lost when vscode converts them. The Lean4 vscode extension rescues those fields by monkey patching the converters:

See: https://github.com/leanprover/vscode-lean4/blob/bbe3ff126cd54defd10ac6e07a2b94dd2d865c42/vscode-lean4/src/utils/converters.ts

This PR uses a more minimal patch in order to rescue just those leanTags and some other fields. This also solves an issue where we had these existing types in waterproof-vscode/src/lsp-client/lean/requestTypes.ts:

`export interface LeanDiagnostic extends Diagnostic {
    fullRange?: Range;
    isSilent?: boolean;
    leanTags?: LeanTag[];
}

but they were never included in the final diagnostics message. Now that they are, the type makes sense.

It then uses those leantags to determine whether a diagnostics message is about unsolved goals. This means we have a flag to determine whether we should hide this unsolved goals error message in the editor (see #332 ). This is more robust then string matching on unsolved goals in the diagnostic. Furthermore, this patching allows us to add more patching similar to the Lean4 vscode extension if needed in the future.

Testing this PR

If you really want, you could inspect the new contents of the diagnostics messages to see the leanTags now being preserved. Otherwise there are some new unit tests.