Completion

[Alizter]

Code completion gives suggestions about what the user might want to type. We need to investigate groups of objects and priorities.

[ejgallego]

Yup, there is already basic support in #41 , but needs more work before merge, and upstream thanks to rocq-prover/rocq#8766

Some more concrete TODOs here:

• we need to refine how to select the completion token from a position. Here we have two cases:
  • the ast for the position at point is available, then we can actually build an interval map and use a fancy heuristic.
  • parsing failed and only a text span is available. Maybe we can still call Coq's tokenizer on that span, but OMMV.
• completion of notations need to build a (cached) prefix map
• map objects to their kinds

[ejgallego]

Also there is the possibility to integrate the work on smart tactic completion that we started in this branch

https://github.com/jscoq/jscoq/commits/v8.15%2Bbernard_tactic_info

Basically that allows to understand what tactics like destruct or inversion may produce, and then complete for the user.

Implementation needs two steps:

• add support for speculative execution to Flèche (that's kind of easy)
• understand the results from the speculative tactic execution

Maybe we can move this to its own issue?

I cc @corwin-of-amber as this may be of his interest.