search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
356 stars 32 forks source link

associated generated errors with pluscal errors #109

Open flazz opened 5 years ago

flazz commented 5 years ago

In the toolbox if the generated TLA code has an error its often possible to jump to the line of pluscal that is the source for the generated error. Is it possible to add this?

alygin commented 5 years ago

I believe this feature is more general — one can jump from TLA+ to the corresponding PlusCal code block even when there were no errors. It would surely be good to have the same functionality in the extension.

The toolbox instantiates a pluscal-to-tla translator directly, so it has access to additional information, including tla-to-pluscal mapping (code) which is used to implement the "Goto PCal source" command.

Unfortunately, this information is not accessible when calling the PlusCal transpiler as a command line tool (the extension works this way).

@lemmy, what do you think about providing the tla-to-pluscal mapping as a part of the PlusCal output?

lemmy commented 5 years ago

@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 make its refactoring more difficult.

alygin commented 5 years ago

I'll have a look at what can be done there.

flazz commented 5 years ago

thanks for clarifying, it is more general, I mostly use it when there are errors.