Do not enclose plaintext in ``` on hover

[ThreeFx]

When working with larger multiple plaintext outputs, enclosing each output in ``` hinders readability.

versus

As far as I am aware, the only "fake" language in this way is "plaintext", every other language should be continued packed in ```. If this is not the case, we can adjust the condition of course.

[martskins]

Which language server are you having trouble with because of this? I'm curious as to why they would use that variant of MarkedString as opposed to using a regular string if they are sending plaintext. So I'd be keen to ask why that is the case before merging something like this.

[ThreeFx]

I'm using the Isabelle/VSCode backend of Isabelle, with a custom connector.

The server include "plaintext" as language tag in the responses:

{"jsonrpc":"2.0","id":1,"result":{"contents":[{"language":"plaintext","value":"Trying \"simp\", \"auto\", \"blast\", \"metis\", \"argo\", \"linarith\", \"presburger\", \"algebra\", \"fast\", \"fastforce\", \"force\", \"meson\", and \"satx\"..."},{"language":"plaintext","value":"Found proof: by simp (0 ms)"},{"language":"plaintext","value":"Found proof: by auto (0 ms)"},{"language":"plaintext","value":"Found proof: by fastforce (0 ms)"},{"language":"plaintext","value":"Found proof: by force (0 ms)"},{"language":"plaintext","value":"Try this: by simp (0 ms)"},{"language":"plaintext","value":"command \"try0\""}],"range":{"start":{"line":6,"character":24},"end":{"line":6,"character":28}}}}

As to why they're doing that: no idea. I could try to ask upstream though.

[martskins]

As to why they're doing that: no idea. I could try to ask upstream though.

This would be very helpful, so if you can do that that'd be great!

[ThreeFx]

I believe upstream does this since VSCode renders plaintext as normal text, and never really thought deeply about it.

It sounds like a good idea to handle this the same way as VSCode though, what do you think?

[martskins]

My only issue with this is that merging this opens the door to supporting all the other extravagant ways in which servers may be sending plain text. What I mean is, I don't think plaintext is actually a "supported" language in markdown (correct me if I'm wrong), so if we add a special case for this then it means we could also potentially see ourselves supporting plain-text, or plain_text, or text, or any other way that some other server is trying to indicate that the text they are sending is just text and not code. I think the correct thing to do here would be to "fix" the server so that is sends MarkedString::String instead of MarkedString::LanguageString, that is, "some example text", instead of { "language": "plaintext", "value": "some example text" }. As for VSCode, I would surprised if it handled this case specifically, what I think might be going on though is that markdown is always rendered in VSCode so you don't get the backticks. I guess as a middleground solution to get something similar to this you could set conceallevel=2 to hide the backticks, although they are not completely hidden.

Let me know how you feel about maybe opening a PR/issue in the server instead, I think it would be the more correct solution. Keep this open until we get to a resolution though, I'm not discarding the idea just yet. Thank you!