Custom suggestions

Stream: lean4

[Kenny Lau]

Following #mathlib4 > bool syntax @ 💬 , is it possible to tweak the VSCode suggestions?

import Lean

syntax "#asdf " (&"true" <|> &"false") : command

-- truman falsify

#asdf t
#asdf f

In this declared syntax, only true or false are allowed, but the VSCode suggestion doesn't know this, so you get:

image.png

image.png

Is it possible to make VSCode only suggest true or false?

[Kenny Lau]

(update: import Lean is not needed)

[Jakub Nowak]

Not sure if completely removing "truman" and "falsify" from suggestions would be possible? But VSCode lists text suggestions last, so if lsp could suggest "true" and "false" as keywords it would ensure they're listed first.

[Jakub Nowak]

This example showcases the problem even more, because "true" and "false" are listed before "truman" and "falsify":

import Lean

syntax "#asdf " (&"truman" <|> &"falsify") : command

-- true false

#asdf t
#asdf f

[Robin Arnez]

you can do... uhh

import Lean

syntax (name := asdf) "#asdf " ident : command

-- truman falsify

open Lean Parser Elab Meta Command

@[command_elab asdf]
def elabAsdf : CommandElab := fun stx => do
  let newEnv := errorExplanationExt.setState (← getEnv) (.ofList [
    (`true, {
      doc := "_"
      metadata := {
        summary := "adfeq"
        sinceVersion := "r8347871"
      }
      declLoc? := none
    }),
    (`false, {
      doc := "_"
      metadata := {
        summary := "adfeq"
        sinceVersion := "r8347871"
      }
      declLoc? := none
    })
  ] _)
  let funnyCtx : PartialContextInfo := .commandCtx {
    env := newEnv
    fileMap := ← getFileMap
    ngen := {}
  }
  pushInfoTree <| .context funnyCtx <| .node (children := {}) <| .ofCompletionInfo <| .errorName stx stx[1]

#asdf true
#asdf false

[Kenny Lau]

:melt:

[Aaron Liu]

very complicated looking