Create new module command not found

[CES-dengzeyuan]

Hi - When I followed the Getting Started, I couldn't find either "Create new module (TLA+)" or "Create PlusCal block (TLA+)" snippet from the drop-down list.

So I wonder how can I get/generate a program demo before I go ahead.

Thanks a lot.

[nano-o]

This indeed seems to be confusing for new users.

[lemmy]

Yes, this is annoying. It looks like the trouble you're facing might be because VSCode loads the TLA+ extension only after opening a .tla file. So, when you have a fresh workspace without any .tla files, the TLA+ extension isn't activated, and that's why the VSCode command emmet doesn't display the TLA+ commands.

[nano-o]

Those commands also don't appear in the command menu even from a loaded tla file on my setup. I'm using the nightly version of the extension.

[lemmy]

Is the editor with the .tla file VSCode's active editor?

[nano-o]

I think so. That's the only open file and my cursor is in it. It says TLA+ at the bottom right of the window. But then I don't know much about VS Code.

[lemmy]

Can you post a screenshot of the VSCode window with the command emmet expanded?

[nano-o]

[nano-o]

Is that what you mean by "command emmet expanded"?

[lemmy]

Thanks, yes, that's what I meant. In the screenshot, the TLA+ commands do show up. When are they missing?

[nano-o]

That's what missing: "Create new module (TLA+)" or "Create PlusCal block (TLA+)"

[lemmy]

Ohh, those two commands also don't show up for me. I have the nightly build of the VSCode extension (not the released one) installed.