Blocker: TLA+ model checking (web) view not populated when model-checking again

[lemmy]

On Windows (and Linux) with VSCode newer than 1.46.1 and any version of this extension in 1.5.0..1.5.1-alpha-2, re-running model-checking results in an empty web view (iff the web view gets closed in between). The Windows task manager confirms that TLC spawns and terminates correctly.

(Downgrading to VSCode 1.46.1 reliably fixes the issue)

[lemmy]

@alygin Any way we can help with this issue?

[lemmy]

I took a stab at this tonight and I agree with the VSCode authors that webviews are a clutch. The issue is gone when, instead of caching the webview, a new one is always created. There are a few issues related to webviews that popped up after the 1.47 release, but they don't fit. Perhaps, the root cause is tightened security related to the resourcePath that somehow becomes invalid?

Here is a radical idea... Why not ditch the error-view in favor of opening (an enhanced) SpecTE.tla in the regular editor in combination with a couple of editor enhancements such as folding, highlighting of modified vars, ... This would also make it a lot simpler to add trace expression evaluation to the extension.

[alygin]

@lemmy, you're absolutely right. The problem is caused by resource paths invalidation after web view closing, and dropping the page source cache solves the issue.

Regarding the radical idea, I thought about possible ways to abstain from using a web view when I just started working on the extension, but I failed to come up with a good UI that would be only based on the text editor features. But VS Code has been rapidly evolving since then, so I guess, some interesting ideas might be implemented now. Though, despite my love of text-based UIs, I honestly don't see how the web view could be completely replaced here without losing usability.

[alygin]

@lemmy, here's a pre-release with the issue solved: v1.5.1-beta.1

Update: And here's the release: v1.5.1

[alygin]

BTW, WebView is finding its way to other parts of VS Code: 46585. I hope it'll become more robust as it becomes more widely used.

[alygin]

Fixed in v1.5.1. Please, reopen the issue if the problem still remains in your environment.