No error highlighting in local lean server

Stream: general

[Siddhartha Gadgil]

I have set up the lean server and am running locally on my laptop. This is with WSL. Everything is working nicely (including adding new projects) except that the red squiggly underlines are missing where there are errors. If I go to the place with the error the error shows up in the infoview.

@Jon Eugster Do you know what could be causing this. In case it helps, I opened a Javascript console in the browser and found the following messages (this was even when the code had no errors):

@leanprover/infoview: "/infoview/index.production.min.js"react: "/infoview/react.production.min.js"react-dom: "/infoview/react-dom.production.min.js"react/jsx-runtime: "/infoview/react-jsx-runtime.production.min.js"[[Prototype]]: Objectconstructor: ƒ Object()hasOwnProperty: ƒ hasOwnProperty()isPrototypeOf: ƒ isPrototypeOf()propertyIsEnumerable: ƒ propertyIsEnumerable()toLocaleString: ƒ toLocaleString()toString: ƒ toString()valueOf: ƒ valueOf()__defineGetter__: ƒ __defineGetter__()__defineSetter__: ƒ __defineSetter__()__lookupGetter__: ƒ __lookupGetter__()__lookupSetter__: ƒ __lookupSetter__()__proto__: (...)get __proto__: ƒ __proto__()set __proto__: ƒ __proto__()
webview.js:1 TODO: catch JSON.parse failure:  SyntaxError: Unexpected token 'e', "esms,true,"... is not valid JSON
    at JSON.parse (<anonymous>)
    at webview.js:1:39063

[Siddhartha Gadgil]

I just saw that if I run with npm start instead of npm run production I get the correct error messages.

[Jon Eugster]

Interesting.Could you add an issue at the gitumhub repo, so I can look at it at a later point, please? Also, of you ise npm production could you check if bubblewrap is installed and if it's being used (you'd see "running without bubblewrap" in the server shell otherwise). Add that to the github issue, I'll try to look at it later this week :)

Pretty sure the "unexpected token e" error is a red hering, that's always there even in a functioning version.

[Siddhartha Gadgil]

I have made an issue. Thanks.