The plug-in shows informational messages both in the "Problems" pane and as green underlines in the source text. However, when this information from Dafny has several lines, the actual multi-line message is replaced by "Dafny VSCode".
Repro:
class {:autocontracts} MyClass {
}
This highlight "MyClass", but each of the three messages just says "autocontracts: Dafny VSCode". When running Dafny on the command line, these tool tips show as follows:
$ dafny /printTooltips MyClass.dfy
Dafny 2.2.0.10923
MyClass.dfy(1,23): Info: autocontracts:
ghost var Repr: set<object?>
MyClass.dfy(1,23): Info: autocontracts:
predicate Valid()
reads this, Repr
MyClass.dfy(1,23): Info: autocontracts:
this in Repr && null !in Repr
Dafny program verifier finished with 1 verified, 0 errors
The plug-in shows informational messages both in the "Problems" pane and as green underlines in the source text. However, when this information from Dafny has several lines, the actual multi-line message is replaced by "Dafny VSCode".
Repro:
This highlight "MyClass", but each of the three messages just says "autocontracts: Dafny VSCode". When running Dafny on the command line, these tool tips show as follows:
Rustan