offer "--filter-position" (and perhaps --filter-symbol) via the IDE

[kjx]

The CLI has --filter-position and perhaps --filter-symbol options to drive verification.

because I have a bad habit of 10,000 line files (or rather projects in just one file - long story)
I tend to use that rather than the IDE verification.

it would be nice if I could click on a line and say "verify here" (i.e. --filter-position)
or on (or inside) a declaration and verify that declaration (ie.. -filter-symbol)

[keyboardDrummer]

or on (or inside) a declaration and verify that declaration (ie.. -filter-symbol)

Can't you already do that? If you set 'automatic verification' to never:

Then you get these clickable icons in the gutter:

it would be nice if I could click on a line and say "verify here" (i.e. --filter-position)

For sure. I hope to build that, but I'm currently occupied with more pressing Dafny work

[kjx]

I don't mean to hassle - and I'm fine with working with the IDE on 2/3rds or the screen and the CLI on the other.

I'd like to direct verification to a single line rather than a whole enclosing declaration: it's often quicker for me..

Also, no idea why the language server (does it stay around) is often slower at e.g. verifying a single method than the CLI. Again I know it's bad practice (long story: waiting til I get to a milestone to refactor) to have a 12k line file - but that means e.g. the pre verification etc happens on the whole file each time, and the IDE appears slower to me at than the CLI...

anyway - I do appreciate what you're doing making the IDE better!

[keyboardDrummer]

I'd like to direct verification to a single line rather than a whole enclosing declaration: it's often quicker for me..

Yes, that's what I'd like to build. However, I don't have a timeline for when I'll do that.

Again I know it's bad practice (long story: waiting til I get to a milestone to refactor) to have a 12k line file

It's worse than you'd think. At the moment, parsing and resolution caching in the IDE only work for code that's in an unchanged file. You will see orders of magnitude improved IDE responsiveness if you use small files.