I rarely use the Toolbox (especially since I couldn't find a pre-built Toolbox for ARM processors). I'm happy with vim or emacs and I usually have a script (that also does some massaging on the PlusCal-generated code): https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/ker...

Frama-C is similar; every one says to use the gui, but I find it horrible and just use the command line while feeling like a cave man.

If it helps at all, I do that a lot too, and have started working on extending my vim plugin[1] to also do configuration and run TLC.

Honestly the big blocker here is learning how vimscript better.

[1] https://github.com/hwayne/tla.vim/

Out of curiosity (and I'm speaking largely out of ignorance on this), have you considered making this plugin NeoVim specific and doing it in another language you are more comfortable with?

EDIT: Also, just realize that you are the person who wrote the Practical TLA+ book...I loved it! Thanks for writing it!

I do it in emacs, have been meaning to write a mode for a while, but.. time.