idris-community / idris2-lsp

Language Server for Idris2
BSD 3-Clause "New" or "Revised" License
164 stars 33 forks source link

Feature Request: Code lens #196

Open ribosomerocker opened 1 year ago

ribosomerocker commented 1 year ago

Code lens are kind of a generic thing, but one example I use in HLS which isn't available here, is

thing :: Int
thing = 2

-- >>> thing + thing

and, on Doom Emacs, a code lens appears next to the last comment saying "Evaluate", and when I click on it, it appends to the file this comment:

-- 4

resulting with

thing :: Int
thing = 2

-- >>> thing + thing
-- 4

Some things worth highlighting:

  1. This code lens only activates when i have three arrows in a comment
  2. after the code lens is evaluated, it says "Refresh" next to the comment with three lines, and clicking on it would regenerate the comment under it, which is useful in-case the value of thing changes, for an example.