vscode expand selection is coarse

Stream: general

[Alok Singh]

import Lake
import Lean

namespace NumeralParser^
  def zero := Lean.Parsec.pstring "zero" <|> Lean.Parsec.pstring "0"
  #eval (NumeralParser.zero)  "0".iter
  #eval (Lean.Parsec.pstring "0" <|> Lean.Parsec.pstring "zero") "0".iter
end NumeralParser

def String.reverse (s : String) : String := s.toList.reverse.map Char.toString |> .join
#eval "a132".reverse = "231a"

hitting the shortcut to expand selection when cursor is at caret (^), it selects the word NumeralParser, then whole namespace first line, then entire file. it should stop at a block boundary

[Eric Wieser]

I'm struggling to find documentation on supporting this feature, but my hunch is that it operates on the textmate grammar, which can't hope to correctly parse Lean code precisely enough for this

[Eric Wieser]

Ah, it's registerSelectionRangeProvider!

[Marc Huisinga]

This is likely because Lean does not implement LSP's textDocument/selectionRange request.

[Eric Wieser]

Ah, so this would need no change to the extension, and only to the language server?

[Marc Huisinga]

Yes, I think so. I haven't double-checked whether VS Code actually uses this request when expanding a selection, but it seems likely.