Navigating and executing

The contents of pcoq windows a structured data. It is different from text in that it handled as tree structures carrying information about each command. This approach makes it easier to have nice mathematical notation and quicker systematic manipulation of commands. For instance, whenever you click in a non-empty window, a complete expression gets selected (you see this because its background becomes grey). This expression is one of the structures manipulated in the window. However, for users accustomed to manipulating text in word processors, it may be very confusing.

The Selection menu

To help with this aspect, the pcoq system provides a specific menu, entitled Selection. The options provided in this menu are organized in two packages.

The first package provides the basic commands to move in the tree structure. Each node in this tree has siblings, a parent node, or children node. Some nodes, called Meta represent holes in the tree structure. One could also say that Meta nodes represent place-holder to fill in. As such they play a central role in the editing process and the Selection menu also provides quick ways to move from Meta node to Meta node.

The second package of navigating options provides more elaborate commands.

The first option, Goto current is used to force the window to display the currently selected expression. In contrast with most word processors or text editors, Pcoq does not insist that the current focus of action should also be the current focus of observation. For this reason, the currently selected expression does not change when the window gets scrolled, for instance with the scrollbars. As a result, one may get to a situation where the currently selected expression is lost in a large file and the user has no clue of where to find it. This option makes it easy to bring the current selection back into view.

Yves Bertot