Errors from widgets

Stream: lean4

[Joachim Breitner]

I’m playing around with writing widgets, and my JS code is certainly buggy. But where would error messages or exceptions or output from console.log be shown in VSCode? I see nothing in Problems, Output or Debug Console.
(Pinging @Edward Ayers who just ran to his bus, but no hurry, I’m wrapping up for today and will tackle that tomorrow.)

[Wojciech Nawrocki]

@Joachim Breitner they will show up when you Open Webview Developer Tools

[Edward Ayers]

Ctrl+Shift+P and then type "webview developer tools", there is also a debugger (which you can trigger with the debugger; keyword.)

[Joachim Breitner]

Spot on, thanks!

[Taro Naoi]

Speaking of devtools, does anyone know how to integrate React devtools into the devtools provided by VSCode?

[Taro Naoi]

Tried a couple approaches, but nothing has worked so far. Currently thinking of using something like this as a way to check for re-renders instead of React devtools: https://github.com/welldone-software/why-did-you-render.

[Wojciech Nawrocki]

Taro Naoi said:

Speaking of devtools, does anyone know how to integrate React devtools into the devtools provided by VSCode?

I was able to get React devtools to work in the Lean4 infoview by injecting the <script> tag that React devtools requires into the infoview html in the vscode-lean4 extension and then rebuilding the extension. It would be cool if it worked without that much fiddling though.

[Taro Naoi]

Nice! Was the <script> injection in the string returned by initialHtml in infoview.ts? Also, did you have to install the react-devtools package via npm?

[Taro Naoi]

I think I tried something like that, but because the infoview is embedded in an <iframe> I don't think it was being picked up by devtools.

[Wojciech Nawrocki]

Taro Naoi said:

Nice! Was the <script> injection in the string returned by initialHtml in infoview.ts? Also, did you have to install the react-devtools package via npm?

Yes exactly, and yes. You also need to run devtools on the command line as their readme indicates.

[Taro Naoi]

Hmmm, not sure why it wasn't working, but if I had to guess, it's because I was running stuff in the windows subsystem for linux and devtools doesn't have access to whatever is running outside of the subsystem. I'll try testing it in a different environment to see if I can get it working. Thanks for the help!