In this quick tour we have missed many important aspects of
the programming environment, such as
- deleting a refinement by means of a delete-command (<#168#>d<#168#>);
- the incremental syntax check during input of new refinements;
- the backtrace facility for semantic errors;
- the edit-on-the fly upon detection of syntactic or semantic errors;
- the trace facility.
We have not discussed useful tricks, such as
- how to change the name of a refinement (take it into the
editor, edit its name, delete the original);
- how to inspect the value of a variable or constant after
execution of the program (focus on its name and show it);
- the use of the <#171#>;SPMlt;BREAK;SPMgt;<#171#>-key to halt execution or input.
Since these are all consequences of things described in chapter
5, it may be useful to read that chapter again.