Support for inline TypeScript #3
Description
Although widget modules are JavaScript code (see here) and can be written in JavaScript directly, JS is more of a compilation target than a source language since the development experience is bad. This is why most of the actual widget sources are written in TypeScript.
However, the only way we can use TypeScript right now is to set up a separate directory like the one I just linked, and invoke an NPM build script (or tsc directly) from Lake. This presents a barrier to entry. Moreover the way we include compilation results in Lean using include_str does not interact well with Lake (although this particular issue should be fixed in Lake).
Happily, it has been demonstrated in lean4-alloy that the Lean 4 language server provides enough hooks to run an entire other language server from it. For us this means that we could provide a custom elaborator typescript!{ ... } which transparently invokes a TypeScript language server (probably in a tmp/ directory somewhere) with the exact configuration (e.g. package.json/tsconfig.json/rollup.config.js) needed to transpile widget code, providing syntax highlighting, autocomplete, etc for TS from within a Lean file, and eventually producing a Lean term of type String for the emitted JS.