tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Markdown with embedded TLA+ #276

Open frankshearar opened 1 year ago

frankshearar commented 1 year ago

VS Code's Alloy extension gives me the ability to embed Alloy code inside a Markdown file. This allows me to produce a model and nicely laid out documentation in the same file. (At the moment I write a prose description of what the model simulates, but I have no ability to add structure to this, like emphasis or sections or whatever.

I'm imagining a UX like where model appears inside tlaplus fenceposts. I could still run "Check with TLC" and all the other TLA+ commands in VS Code, just within a .md file instead of a .tla file. Either the configuration could stay in a .cfg file or appear within the file in atlaplus fence.