feat: picker-based input method for abbreviations in non-editor contexts#762

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom

mhuisi:push-upmprtpksvuumhuisi/vscode-lean4:push-upmprtpksvuuCopy head branch name to clipboard