In this page, you can learn about general properties of structure navigation, abstract syntax, menu-guided editing, auto-clipping, using the X copy-paste mechanism, text editing, and adding comments. You may also be interested in following a short tutorial on editing. From here, you can also go back to the help summary.
CtCoq is built on top of Centaur, a programming environment generator where the structure of programs is more important than their textual form. This characteristic makes it easier to develop advanced features like powerful notations, proof by pointing, script management, and natural language explanation of proofs. On the other hand, the user needs to understand that the commands he or she enters in the system will always be manipulated as tree-like structures.
In this document, we describe the various commands that make it possible to edit structures. We also show that the more usual form of textual editing, as it is practised in most program editors, can also adapt in this structured environment. Thus, users who want to know as little as possible about structure editing and prefer to keep a text-oriented behavior can jump ahead to the section on text editing.
Whenever you click inside a CtCoq window with the left button of the mouse (and no <Shift> or <Control>modifier , you select a complete syntactic sub-expression of the window content. Thus, there is no notion of cursor, but a notion of currently selected expression. Clicking is a way to move this current selection around, but there are also keyboard actions:
| ^B | Tree left (move backward) | ^F | Tree right (move forward) |
| Escape ^U | Tree up | Escape ^D | Tree down |
| Escape p | Move to previous hole | Escape n | Move to next hole |
Once an expression is selected, it is possible to hide it by choosing the option "Shrink" from the Selections menu. On screen, the selected expression is then replaced by "...". This operation does not actually perform any modification on the expression, only on the way it appears on the screen. It is then possible to make this expression reappear by choosing the "Expand" option in the same menu. The State and Theorem windows do not have a menu bar attached, but they have the Selections menu attached to a special mouse binding.
This shrinking mechanism works hand in hand with a general mechanism to hide parts of terms on the screen. The user can actually specify a printing depth that makes that all sub-expressions at a given depth in the structure displayed in a given window are compressed and replaced by the short string "...". This printing depth parameter can be modified at will using the Set Print Level option of the Display menu from the menu bar. For the windows State and Theorems this menu can be had using another special mouse binding.
Being a tree-like structure, every expression has a head operator and some number of child expressions. The language also provides a range of syntactic categories, also called phyla (singular : phylum), which correspond to sets of accepted operators. These phyla make it possible to distinguish between several possible syntactic contexts. There are several kinds of operators. Some operators (like the operator for universal quantification, for instance) accept a fixed number of child expressions (two for the universal quantification), which may be of different phyla (BINDER for the first child, FORMULA for the second child). Some other operators (for example the operator id_list used in the Intros tactic) can have an arbitrary number of child expression all constrained to belong to the same phylum (here ID, which contains only the operator for identifiers)
The basic capabilities to modify tree structures are given in the "Edit" menu from the menu bar. Having selected an expression you can copy this expression to the clipboard with the "Copy" option. It is then possible to move the current selection in another place and to paste the copied data, by using an option chosen between "Insert <", "Insert >" or "Change". Note that the "Insert" options are available only if the target position is under a list operator. The pasting of the copied data occurs only when the head operator of this data fits in the expected phylum at the target position.
The interface provides a set of menus that enable you to introduce command or formula templates in your commands. These menus are available when you choose the options "Beginner" or "Expert" in the Editing-Tools menu. The options provided in these menus are transformation rules that can be applied on the current selection. The set of proposed options is always adapted to the phylum describing the context of the current selection, so that this menu editing tool provides help to construct only commands that respect the syntactic constraints. To understand more about this menu-guided editing tool, it may be interesting to look at a simple tutorial.
In most windows, the middle button of the mouse has been reserved to provid a Copy-Paste shortcut to the Command window. When the user selects with the middle button a expression e, then this expression is automatically copied and pasted at the position given by the current selection in the Command. This behavior is coherent with a behavior of the window as a template menu for itself. However, this behavior is not compatible with the X copying and pasting mechanism and novice users may be surprised.
The X-window system also provides functionalities for moving text between windows from various applications. Our windows are (partly) compatible with this mechanism, although the bindings of the mous buttons are changed with respect to the usual X-window convention. To copy the text representation of a tree-structure in the inter-application buffer of X-window, users only need to depress the <shift> key while selecting this tree-structure with the left button. To replace a term with the contents of the X-window buffer, users only need to depress the <shift> key of the keyboard while selecting this position with the middle button of the mouse. This behavior departs from the X-window conventions in its use of the <shift> key.
Using these functionalities, it is very easy to copy and paste data between the CtCoq interface and any other text editing tool. However, this communication mechanism does not yet work when performing text editing in the interface.
At any time (there are very few exceptions), the user can select an expression and decide to edit the text of this expression as if it was a plain text fragment. Text editing is provided in the Command windows as soon as the user types a regular character or escape t. All the key bindings for this window disappear until the window returns to the standard behavior.
When entering text-editing mode, the selected tree is replaced by a text area containing its textual representation(on a green background). For formulas, this also means that special characters like quantifiers and logical connectives are replaced by the corresponding ascii conventions, coming back to the regular syntax of the Coq proof assistant. A cursor (on a grey background) is also placed at the beginning of this text area. Thus the window content takes the following aspect:
As can be noticed in this example, extended notations are used only outside the text area.
The text editor is very rudimentary. It makes it possible to move the cursor around using the mouse and it provides a few key bindings similar to the bindings usually found in the Emacs text editor:
| ^A | Move to beginining of line | ^B | Move Backward one character |
| ^D | Delete current character | ^E | Move to end of line |
| ^F | Move forward one character | ^G | Abort text editing |
| ^H (backspace, Delete) | Delete previous character | ^K | Kill to end of line |
| ^M | New line | ^N | Move to next line |
| ^P | Move to previous line | <Escape> | Parse and exit text editing |
This text editor cannot receive the X copy-paste buffer selection. Thus, the X copy-paste mechanism can only be used in structured editing.
when a satisfactory text fragment is reached, it must imperatively be parsed, using the <Escape> key, to be validated. A tree structure corresponding to this text fragment is constructed and the expression that was initially selected is replaced by this tree fragment. This parsing operation may fail, and in this case an error messages is reported in the Centaur messages window.
It is also possible to request that a command be sent to Coq without explicitely parsing it. For this, it is only necessary to type ^C g (Control C, then g). The user-interface will parse the text fragment before sending it to Coq.
While in text editing mode, it is possible to move the cursor in the text area, as we already mentionned. However, it is also possible to select an expression outside the text area. If this happens, the interface leaves automatically the text editing mode and the default key bindings become valid anew. In particular, it is possible to type ^E again and to start text editing on another expression. This way, it is possible to start editing text on several expression at a time and to proceed by placing the cursor in the text area of interest. This possibility to edit several expressions at a time may be overwhelming to beginners.
Comments are only partly supported in CtCoq. When parsing a file, all the comments that are attached to commands are kept, but the comments that appear inside tactics or logical formulas are lost. When editing commands in text editing mode, it is possible to add comments before these commands by simply typing the conventional tokens for starting and terminating comments: "(*" "*)". However, the parser is a bit high handed with comments, so that several comments attached to the same command are considered the same as one multi-line comment, with only one starting "(*" and one terminating "*)", also white space at the beginning of a comment is not always well respected Still, correctly nested comments are well managed.
In the CtCoq windows, the tokens for starting and terminating a comment do not appear. Instead, the comment can be distinguished from the regular commands by a change of background and a change of font. The tokens for starting and terminating comments are only restored when saving the window content in a file in plain text format.