search

tirix / metamath-vspa

A Visual Studio extension and LSP server for Metamath
MIT License
3 stars 0 forks source link

Wrong hover descriptions on constants #8

Open tirix opened 2 years ago

tirix commented 2 years ago

In general, the correct description is provided when hovering over constants:

image

However, in some cases, there is a shift between the correct description and the description shown:

image

Here, the correct description for /\ would be: Wedge (read: 'and') But the description shown is: Vee (read: 'or')

tirix commented 2 years ago

The reason is that metamath-knife expects the comment for a given statement just before that statement, as it is systematically the case for all axioms and theorems. However in the case of many constant declarations (but not all), it is provided just after them.

Obviously there is a more general question here, about whether we shall have a strict formatting for comments associated to $c constant declarations, or implement a kind of empirical rule (like, "if a comment follows on the same line, it is the associated comment").

I don't expect this issue to be fixed quickly, and there will probably no change to be done on the Visual Studio Code extension or LSP server, but I wanted to track it anyway since it will probably raise questions.