Markus Alexander Kuppe

https://www.youtube.com/watch?v=pTN3nHvSm84 /cc @quaeler

A similar problem if opening bracket of define is on the next line: ```tla define { ... } ``` See https://github.com/lemmy/azure-cosmos-tla/blob/6e4e505a663ced50a61120219a70c7a2c1ae0f17/general-model/cosmos_client.tla#L84-L85

This is what works for the Toolbox trace explorer: https://github.com/tlaplus/tlaplus/blob/6bc82f7746ccdfbdf49cdef24448666d11e5e218/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java#L82-L121

@alygin Not impossible but nothing I can commit to in the foreseeable future. The way how TLC reads specs into (sub-)actions causes confusion in a couple of places (coverage, ...).

@alygin I see no reason why we wouldn't accept a PR that makes the pcal mapping universally usable. Unfortunately, I believe the feature doesn't have good test coverage which will...

Try Settings: tlaplus.pdf.convertCommand

1) I can't think of a reason why I would need the file. On the contrary, the back-end sends the absolute path of the file to the front-end. 2) If...

+1 for "attach to a running TLC process from anywhere". When debugging, the web view panel doesn't provide much value. Thus, iff allowing concurrent debugger sessions is desirable functionality, it...

You can install the nighty/latest VSCode extension (with a recent snapshot of TLC) from https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus-nightly.

It is the fourth button on the top row of `Readme.md` (https://github.com/tlaplus/vscode-tlaplus/commit/932a0f6f63bd66ee7c58456245e24af20085eac5). Can you open a PR that better highlights the nightly release in the `Readme.md`?