Hi Chris,
You wrote (approximately):
>>Your REPL seems to be a specification editor based on the TECO model,
>>treating the screen as a glass teletype.
It's more than that, because of
(1) the ability to very easily evaluate expressions at any time, using
the definitions you've built up so far.
(2) the speed of iteration (including staying focused on the keyboard,
rarely using the mouse).
This REPL business is a time-wasting distraction. Anyone who would
rather write a specification (or a program) in TECO rather than in
Emacs is so many standard deviations outside of normal that I'm not
concerned with his or her preferences. Emacs is not a REPL, but when
I use it I rarely use the mouse. I'm not focused on the keyboard; I'm
focused on the document I'm writing--something that would be hard to
do if I couldn't see it. (I've used a REPL theorem prover. It was a
nightmare because I was creating a current state with my typing, but
there was no easy way to see that state because all I could do was
type commands that would show me little pieces of it--like individual
definitions.)
So, whatever specification a user creates will be by editing the .tla
file using a window on the file, as in Emacs. So, lets consider (1).
After setting up a suitable model, when editing in the Toolbox, at any
time with two mouse clicks you can go to the Evaluate Constant
_expression_ part of a model, type an _expression_, run it (one more mouse
click), and read its value. This is not what I'd call difficult. As
for (2), iteration consists of going back to where I was in the
spec--1 mouse click. The speed of iteration is a problem because the
only way to evaluate an _expression_ is by running TLC, which requires
starting a new JVM. No interface change is going to eliminate that
problem. Fixing it requires a significant rewrite of TLC, and perhaps
of SANY if you want to avoid reparsing the entire spec--or use of
another tool.
So, all a REPL buys you is eliminating three mouse clicks with a
little typing. Even I could probably figure out how to replace those
mouse clicks with keystrokes--if someone can specify precisely what
those keystrokes should do. (For example, what if there are multiple
models open?)
So far, I don't think that the current discussion has revealed any
gaps in the functionality that the Toolbox provides. It has pointed
out two problems:
1. The functionality is not well document.
2. It should be possible to use keystrokes instead of some
mouse clicks.
3. Evaluation with TLC takes too long.
I'm open to precise, well thought-out suggestions for improving 1 and
2. It would be great if someone would volunteer to solve 3, now that
Markus has suggested how it might be done.
Leslie