Truncated quick navigate info

Answered

I have a DocumentationProvider that resolve symbols and can show their signature in a quick navigate doc popup (ctrl+hover):

But the doc is always truncated! The full signature is

inductive * mutual_inductive_body * one_inductive_body -> bool

I'm not using fancy html code, the doc variable in next screenshot contains the exact html returned by the provider:

Another example:

This is on 2020.1, but I got the same problem on 2020.2 too.

Any idea ? Do I have to use some special markup elements ?

0
3 comments

Thanks for pointing that issue, but I'm not sure it's the same.

I have the problems in 202 and 201, and I'm not using 203 yet.

Also in the latest screenshot you can see that the text is not long at all.

 

0

Please file a separate issue then. It might also be related to specific OS/graphics/monitor scaling.

0

Please sign in to leave a comment.