Hello,
Thanks for the plugin. Being able to use the JetBrains IDEs (GoLand for me) for TLA+ is a massive improvement over the Toolbox UI in terms of developer experience, especially for people with a non-optimal eyesight. There are a few editor improvements I noticed could make it even better, if you are interested:
- outline / folding support. For example, in PlusCal, it would be nice to have folding available on various levels, including
process, labels, with, while, if / then / else, (fair) algorithm, and the complete code translation.
- Brace matching: being able to use brace matching (^M) to navigate from one extremity of something foldable (e.g. process) to the other extremity would be nice
- individual and global folding/unfolding / filtering in the output window, based on the
@!@!@STARTMSG 2200:0@!@!@ / @!@!@ENDMSG 2200 @!@!@ matching, like you appear to do for the error trace already.
Also, a couple of extra features could be useful:
- the ability to render to PDF (tlatools.jar tla2tex.TLA + pdflatex)
- the ability to evaluate global constant
Foo like the Toolbox: can be done like the toolbox with a temporary model generated on the fly or, possibly more simply, by temporarily adding a ASSUME PrintT(<<"$!@$!@$!@$", Foo>>) before running, grepping output for it, and stripping the wrapping around the result
Hello,
Thanks for the plugin. Being able to use the JetBrains IDEs (GoLand for me) for TLA+ is a massive improvement over the Toolbox UI in terms of developer experience, especially for people with a non-optimal eyesight. There are a few editor improvements I noticed could make it even better, if you are interested:
process, labels,with,while,if / then / else,(fair) algorithm, and the complete code translation.@!@!@STARTMSG 2200:0@!@!@ / @!@!@ENDMSG 2200 @!@!@matching, like you appear to do for the error trace already.Also, a couple of extra features could be useful:
Foolike the Toolbox: can be done like the toolbox with a temporary model generated on the fly or, possibly more simply, by temporarily adding aASSUME PrintT(<<"$!@$!@$!@$", Foo>>)before running, grepping output for it, and stripping the wrapping around the result