designates the script area, 
designates the tentative area, and 
designates the buffer area.In this page, you can learn about the various tools provided to help you to maintain a coherent script, the basic actions, how to buffer several commands, how to undo and to abort an unfinished proof, various accelerators, and tools to help you break down the script in several files.
The goal of script management is to help you record a coherent sequence of commands that will help you replay the proofs performed in your current session. To this end, the interface attempts to record all the commands that you send to the Coq proof assistant, discarding the commands that do not affect the logical state and the commands that you request to be undone.
The script management tools works by placing the commands sent to the proof system in a special zone, the script area. This zone is "read-only", so that you can copy from it but you can't modify the commands it contains. This restriction ensures that the commands recorded there will not be corrupted, even in erroneous manipulations. Since the interface process works in parallel with the Coq proof assistant, it is possible to continue editing and sending command while the proof assistant is busy working on a previous command. To provide a healthy behavior in this context, the interface uses two other "read-only" zones, the tentative area and the buffer area. The tentative area contains the command that is currently being processed by the proof assistant (when such a command exists). The buffer area contains the commands that the user requested to be sent to the proof assistant, but which cannot yet be processed because the proof assistant is still busy with another command. These areas are shown in the following picture, designates the script area, designates the tentative area, and designates the buffer area.
Whenever a command is executed or undone or whenever the Coq proof assistant answers to a command by an error, these areas are reshaped to take into account the modification in the various commands status. Users can thus act on these areas by executing or undoing commands or by resetting.
The "Do it" action can be triggered by clicking on the button "Do it" from the toolbar between the Command and State windows or by typing "G" (<Shift>G) while the mouse is in the Command window. It provokes the selected command to be inserted in the tentative area while it is processed by the proof assistant. The answer of the proof assistant may be an acknowledgement: "Done". In this case, the command is moved from the tentative area to the script area (or, more often, the script area is extended over the command). Alternatlively, the answer of the proof assistant may indicate a failure to execute the command: "Error". In this case the command is simply restored to the area it belonged to before.
When adding a new command to the script area two cases may occur. The first case is when the new command is the first command immediately after the end of the script area. In this case the script area is simply extended over this command. The second case is when the new command is elsewhere in the window. In this case, the commad is copied to the ehnd of the script area. This ensures that the script will be coherent.
Complications can occur because of possible race conditions between the proof assistant and the user. While the proof assistant is busy working on a command, the can edit and send extra commands. These new commands will have to be kept in the user-interface and sent to the proof assistant in the right order as soon as the proof assistant is available. The buffer area serves this purpose.
The "Discard" button makes it possible to cancel the effect of commands already sent to the proof system. It works differently depending on the area in which the last command sent resides:
It is also possible to request that several commands be undone, by simply clicking several times on the button "Discard". The user-interface will simply record the right number of requests and send them to the proof assistant. However, when the commands to discard are definitions, it may be more interesting to use the "Reset" mechanism.
The action of the button "Abort" interrupts the current goal directed proof. this tantamount to cancelling all commands back to the previous Goal command. The script mainteance tool takes this int account and shrinks the script area accordingly.
There are two possibilities to reset to a previous state provided by the user-interface. One is simply to select the command defining a new object in the script area and to type "R" for "Reset". The second possibility is to edit a Reset command using the usual editing means and to execute it using the "Do-it" button. If the corresondponding definition is stored in the Command window then the script is correctly updated. If the reset definition is not in the Command window, the script area is completely cleared awy. This a conservative behavior: there is no way to know for sure which commands in the script area are older than the reset definition and all protection is removed. If this happens to you, you are left alone to take care of the coherence of your work and all restrictions are removed.
There are commands that have an effect on the state of the Coq system but that cannot easily be undone, likeAddPath,DelPath, and Cd.
All the commands that alter the output of the theorem prover must absolutely be avoided. In the current version, the commands Focus, Unfocus,Begin Silent, and End Silent fall in this category.
As mentionned earlier, it is possible to send several "Do-it" requests in a row, without waiting for the Coq proof assistant to synchronize. It is also possible to send several consecutive commands by simply selecting all these commands and sending one "Do it" request, either by clicking on the "Do it" button or by typing "G".
It is also possible to request for the whole content of the Command window to be executed, without having to select it all, by typing "A" (for "do it all") while the mouse is in this window.
During large proof developments, the size of the script tends to become a problem. It is possible to reduce the size of the script present in the Command window, storing a fragment in a file and replacing this fragment by a reference to this file.
The user only needs to select the relevant subpart of the script and type B (for "Build load file"). This propmts the user for a file name, checks that this file name is valid, and inserts a command "Load <file>." in the script area. This makes sure that the script area still contains a reference to the removed definitions and commands.