This PR adds auto-completion for the fields of structure instance notation. Specifically, querying the completions via Ctrl+Space in the whitespace of a structure instance notation will now bring up the full list of fields. Whitespace structure completion can be enabled for custom syntax by wrapping the parser for the list of fields in a structInstFields parser.

This PR also makes completions of partial structure fields in the bracketed structure instance notation work again (e.g. completing a in { a }). These were previously broken by the introduction of set notation.

In order to facilitate language server support for ambiguous syntax where all associated elaborators fail, this PR introduces the notion of an InfoTree choice node and an InfoTree PartialTermInfo node. Choice nodes are produced by the elaborator when several overloaded elaborators fail and contain the InfoTrees of each failed elaborator as subtrees. PartialTermInfos are generated when an individual elaborator fails to produce an Expr so that the subtrees produced by that elaborator can be retained as children of that PartialTermInfo.

Since the InfoTree contains more similar CompletionInfos after the introduction of choice nodes, this PR reworks the CompletionInfo selection to be more effective at selecting the best CompletionInfo amongst multiple similar ones.

Finally, this PR splits Completion.lean into several files and fixes #5807.

Breaking changes

• Lean.Elab.withInfoContext' and Lean.Elab.Term.withInfoContext' gained a new parameter mkInfoOnError that is used to produce an InfoTree node when the elaborator x fails. In cases where mkInfo produces a TermInfo using Lean.Elab.Term.mkTermInfo, mkInfoOnError should produce an equivalent PartialTermInfo without an Expr using Lean.Elab.Term.mkPartialTermInfo.
• Lean.Elab.Info gained two new alternatives: ofPartialTermInfo and ofChoiceInfo.
• The id field of the fieldId alternative of Lean.Elab.CompletionInfo has been turned into an Option with none representing a full field completion.
• The syntax of structInst and whereStructInst have been adjusted to use the structInstFields parser.

Details of other changes

• Init/Prelude.lean and Init/Meta.lean: Add two new functions getTrailing? and getTrailingTailPos? to work with the trailing whitespace of a SourceInfo / Syntax.
• Lean/Elab/App.lean:
  • Adjust dot completion of a.b.c so that the CompletionInfos for a.b.c reference the syntax a, a.b and a.b.c respectively, instead of all referencing a.b.c. Before, these CompletionInfos were indistinguishable and we only chose the right one by accident.
  • Adjust mergeFailures to produce an InfoTree with an ofChoiceInfo root node and the InfoTrees of all failed elaborators as subtrees instead of throwing them away.
• Lean/Elab/BuiltinTerm.lean: Adjust elabCompletion so that it always produces an identifier CompletionInfo, even when elaborating the left hand side of a dot completion succeeds and we also add a dot CompletionInfo to the InfoTree. With the changes to the CompletionInfo selection in the language server, the language server will now always pick the correct one of these two. Before, we had a special case in the language server dot completion where under certain circumstances we would treat it a dot completion as an identifier completion instead - with this change, this is now not necessary anymore.
• Lean/Elab/MutualDef.lean: Adjust expandWhereStructInst to set reasonable SourceInfos for the produced bracketed structure instance notation. The structure field completion benefits from this SourceInfo.
• Lean/Server/RequestHandling.lean: Adjust handleCompletion so that in the - completion case, we also emit CompletionInfoData. This fixes PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item  #5807.

Due to the changes to the structInst and whereStructInst parsers, this PR needs two stage0 updates.