[tlaplus] Open an existing spec - does it work in the TLA+ Toolbox?

[Tatiana Racheva <tatiana.racheva@xxxxxxxxx>]

I found a discussion from 2014 that indicates this was a problem in the past but that it has since been fixed. But, in 2024, I seem to have this problem again.

The only thing I can do is create a new module, either using the File->Open Spec... menu options, or the Spec Explorer.

I'm on Ventura 13.5.2. My TLA+ Toolbox is `Version 1.7.1 of 31 December 2020`.

`java --version` prints:

openjdk 21.0.2 2024-01-16 LTS

OpenJDK Runtime Environment Temurin-21.0.2+13 (build 21.0.2+13-LTS)

OpenJDK 64-Bit Server VM Temurin-21.0.2+13 (build 21.0.2+13-LTS, mixed mode)

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a9f563d3-461d-49d4-aea7-1a887383a702n%40googlegroups.com.