search

tlaplus / vscode-tlaplus

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

Debug variables tooltip and copy #224

Closed fritzalder closed 3 years ago

fritzalder commented 3 years ago

Love the extension (and the new debug feature works great so far)! I found two small issues with the debug window:

  1. In the Run and debug window during debugging, the "Copy Value" option on right click does nothing. As far as I clicked around, no values are ever actually copied to the clipboard.
  2. Hovering on the values of a variable only sometimes gives the correct complete value. Looking at the snip below, Hovering over <<[term |-> 2 ... ]>> gives the correct full value, but hovering over [term |-> 2, ... ] gives the (probably default) "RecordValue: a record" value.

image image

I didn't find a duplicate of this issue, sorry if this is already fixed.

lemmy commented 3 years ago

@fritzalder Thanks for the feedback. Please check if the issues are addressed in https://github.com/lemmy/vscode-tlaplus/releases/tag/v1.6.0-beta.202106014 If yes, I will open a PR for this repo.

fritzalder commented 3 years ago

I just realized that hovering over the variable name gives you an information about its type (RecordValue, IntValue, TupleValue etc) and hovering over the value gives you the content. So my (1) above was not even a bug, I just did not realize this.

But the (2) is fixed by your new version! Copying now seems to work in all cases for me. Thanks for the quick response.

lemmy commented 3 years ago

IMO this issue (the fix is in tla2tools.jar) highlights why the VSCode extension should move away from bundling tla2tools.jar (eventually, it will also blow up the git repo), or at least should make it super easy for users to switch between different tla2tools.jar. Additionally, I propose to create a -nightly release of the VSCode extension in the VSCode Marketplace.

alygin commented 3 years ago

@fritzalder, thanks for the feedback. I hope your problem is solved, so I'm closing the issue. But feel free to reopen it if you think it's not resolved yet.

@lemmy, thanks for the fix. And sorry for being slow on coming up with the nightly version of the extension, we'll do that.

alygin commented 3 years ago

The fix is available in the v1.6.0-alpha.2 pre-release.