In the event that no other interaction method is available, it may be worth providing a low-level command entry window. This is most likely to be required only for communicating with the proof assistant, and would require the user to know the specific language used within. If at all possible, interaction using this method should not be required.
If all else fails, the interface should degenerate to the underlying command-line prompt. Leaving this option available may have some benefits for expert users who prefer the command line interface. Some level of macro commands and scripting may be available from the user's operating system.
|
|
|