Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multi-line information not shown #46

Open
RustanLeino opened this issue Apr 18, 2019 · 0 comments
Open

Multi-line information not shown #46

RustanLeino opened this issue Apr 18, 2019 · 0 comments

Comments

@RustanLeino
Copy link
Contributor

RustanLeino commented Apr 18, 2019

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

Rustan

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants