Skip to content
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

fix: better timeouts #139

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

fix: better timeouts #139

wants to merge 2 commits into from

Conversation

joneugster
Copy link
Collaborator

@joneugster joneugster commented Oct 27, 2023

WIP changes to improve timeouts or connection issues.

The desired behaviour in this first step would be that if the internet connection is broken, then nothing happens but the editor is still visible and selectable. In a second step, a pop-up like in lean4web could be shown.

Addresses #134, #136, #138

Comment on lines +331 to +340
// Catch loss of internet connection
try {
const editor = React.useContext(MonacoEditorContext)
const model = editor.getModel()
if (!model) {
return <p>no internet?</p>
}
} catch {
return <p>no internet??</p>
}
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should eventually be replaced. Currently the oneLineEditor still causes troubles because of an undefined uri

@joneugster joneugster added the abandoned Currently no intention to take this up again label Jan 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
abandoned Currently no intention to take this up again
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant