Vtec234
commented
1 year ago Hi! As you observed, infoview/main.tsx includes stylesheet and font files. This is possible in the extension because VSCode includes a special mechanism to load files from the distribution folder (dist/ in lean4-0.x.y.z.vsix), and our build process places the stylesheet/font in that folder. You cannot easily do a similar thing in a user widget. However, something you should be able to do is simply include the source of the font/stylesheet/whatever as a Base64 string in your JavaScript file, and then load that dynamically. Various bundlers support plugins that can include Base64 encodings of resources in the JavaScript outputs of the bundling process. Here is one resource about this among many.
You may also find EdAyers/ProofWidgets4#8 relevant.
kokic
As a formal tool closely related to mathematics, Lean has many advanced features in its user interface, especially in interactive design. A natural need is to consider displaying $\TeX$ style typesetting in infoview (E.W. Ayers has also had such an idea in the past). Recently, I have been exploring the possibilities of infoview, such as making it display the previously mentioned beautified formulas or even some non-trivial commutative diagrams. Currently, I have encountered a problem that is not critical but makes me very concerned - What is the correct way to load font files in Lean infoview?
I fully understand that infoview is essentially a web page element, and external React components can be added to infoview through User Widgets. If it’s just
.jsor.cssfiles, it works well. However, for font files like.ttf, I’m not sure which directory to place them in so that they can be correctly loaded by React/infoview.I think this has to do with the path because once I change the css (and the path of the ttf file) to a network request like jsdelivr, everything works well.
On the other hand, when I use local css, the style can be loaded, but the font file is missing (even if I put them in the correct path relative to the css source file and also configured related options during packaging).
$\mathbf{Remark.}$ Perhaps I misunderstood the correct way to handle this issue with React components. I noticed that infoview itself also uses local font files, so I believe this is also completely feasible for users.