Skip to content

Auto-complete roles in Verso docstrings #544

@alok

Description

@alok

In

import Lean
open Lean Elab Command
set_option doc.verso true

/--
{lean}`aa` works and so does {lean}`hello`
-/
def aa : String := "aa"
/--
{lean}`fwdDecl` works and so does {lean}`aa` but not {CURSOR IS HERE}`mispelled`
-/
def fwdDecl := 2

If my cursor is in the {}, I tried hitting ctrl-space to get suggestions on what available roles are, but nothing came up. Is it possible to have completion for that? I find it especially helpful for DSLs since docs can be sparse.

Image

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions