Syntax autocompletion

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Since Lean syntax is extensible, there is no easy way to write it down or discover what is valid at any point in a Lean program. Therefore I propose we add a syntax element to the LSP for completion prompts. We could use different icons to represent "syntax" from "members".

Steps to Reproduce

Expected behavior:

show the user that the keyword "where" is allowed here.

Actual behavior:

it only shows 'members' of current namespaces...

Reproduces how often:

The problem is where is not documented in the theorem proving book, and our reference docs are very incomplete, so there is now way to know the where clause is valid here unless you go an read all the Lean compiler source code and new users shouldn't have to do that.

Versions

Lean (version 4.0.0-nightly-2021-12-13, commit 3a6cc774241b, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start with the reported where completion case and the linked screenshot, using the listed Lean version as the reproduction target. The issue names no files or tests, so first locate the LSP completion entry point and determine how syntax completions should be represented. Done means the completion UI identifies valid syntax such as where, with a distinct presentation from namespace members.