LanguageClient-neovim
LanguageClient-neovim copied to clipboard
Do not enclose plaintext in ``` on hover
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.
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.
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.
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!
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?
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!