-
Notifications
You must be signed in to change notification settings - Fork 48
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[issue-114] Infoview should indicate when server is not started #159
Conversation
Hi! Thank you for looking into this! This is still a draft so I am a bit early to comment, but I just wanted to check-in to see where the changes are headed. I was surprised to see the changes in |
(If the reason is to support multi-server workspaces, I think something like this makes sense and if it works, great. We will however need more changes to really support that. For example there is only one |
Thanks @Vtec234 for your comments! (the more the better so no worries). Yeah, at the beginning I just wanted to add the message inside main.tsx but even though the message is displayed correctly ("server unavailable...") the section containing "All messages" remains static (and maybe it's a bit confusing for the user to keep seeing this section if the server is dead), that's why I was checking to change info.tsx logic, until now I'm blocked because I need to catch the exception related to microsoft/vscode-languageserver-node#825. Still investigating another alternatives :) |
Also, if you terminate the server manually the main.tsx is not updated anymore, so maybe we need to add more logic for re-render this part |
Update: Mariana and I figured out a solution by adding a new |
Yes, the watchdog process is meant to never crash unless we have a bug in Lean core, whereas worker processes may crash given inputs such as the |
Having said all that, I took this PR to be fixing what happens when the watchdog (i.e. |
I agree, I filed this as a new issue #175, just so we can get this one finished sooner than later. |
@gebner solved this discussion: #159 (comment) |
@gebner, this should be good to go. |
Thanks! |
This PR contains the next adds related with issue #114 :
Note: This PR needs to merge #162 before merging it.