Add widget effect support for specifying location of text to insert.#234

gebner merged 2 commits into

leanprover:masterleanprover/vscode-lean:masterfrom

EdAyers:insert_textEdAyers/vscode-lean:insert_textCopy head branch name to clipboard