File Edit View Options Utils

Overview of the menus

Alfa's main editing window has a menu bar contaning the following menus:

[Menu bar image]

Below, we give a brief description of the purpose of all the commands you find in these menus.

The File menu

[Menu bar image]

The Edit menu

[Edit menu image]

The edit menu contains the following editing operations, some of which should be familiar from other editors.

The last two commands are only applicable when a place holder is selected, but there is no visual feedback for this at present.

[Menu bar image]

The View menu

[View menu image]

[Menu bar image]

The Options menu

[Options menu image] These commands affect how you input commands when a place holder is selected and what is shown in the menu window.

Input Mode

This is the original mode, where each command is assigned a unique keyboard shortcut, which is displayed in the menu window. A problem with this solution is that the abbreviations are computed dynamically and the same command can be assigned different abbreviations in different context. This means that you have to look in the menu all the time to find out what to type, and this slows down the editing. (The first character in the abbriviation is always the same, so you can always enter the first letter of an identifier without looking in the menu...)
Completions (Under construction)
In this mode, a text entry field appears on top of a place holder when it is selected. You have to enter the full commands, but there is a completion mechanism that fills in the rest when you hit the Tab key, if there is only one matching command, or displays a list of matching commands in the menu window, if there are several. The up/down arrow keys steps throuh the list of available commands. You may have to hit the F1 key to activate the text entry field. (Clicking in the field doesn't seem to work...)

Menu mode

These options control what is shown in the menu window.
Show everything in scope
All identifiers in scope are shown. Status lights (red and green) indicate which identifiers can be used to refine the selected place holder.
Show everything, no status
As above, but the status lights are omitted. Use this if computing the status light is too slow.
Filter through type checker.
This is the original mode where only identifiers that can be used to refine the current goal are shown. This can be slow if there are many identifiers in scope.
If Alfa becomes too slow when you make big proofs, selecting Completions and Show everything, no status is likely to make it a lot faster.
Only refinements from context
Although it is based on the lambda calculus, the expression language used in Alfa is enriched with a number of constructions, such as records, projections, data types, case expressions and local definitions. With this option turned on, most commands to construct these fancy kinds of expressions are removed from the menu, leaving commands to construct terms in the pure lambda calculus. This might be useful when you are working with a plugin module based on a simpler expression language.

Menu Language

Plugin modules can supply alternative ways to display the commands that appear in the menu window. These options allows you to select which view to use.
When no plugin modules are active, this is the only option.

(At the time of this writing, this possibility has been used only in the GF plugin, which allows expressions to be translated into various natural languages. This is why this options are referred to as languages.)

Auto Solve Constraints
When a place holder is instantiated, constraints may arise on the possible values of other place holders. When this options is switched on, such constraints are solved and the affected place holders are instantiated, in cases where this is safe, i.e., there is really only one possible solution. When this option is off, no constraints are solved automatically. Instead, commands to apply the automatic solution appear in the menu. You can also manually instantiate the affected place holder. This gives you more control, e.g. if you have a definition a = b and a constraint ?1 = b, the automatic constraint solver would instantiate ?1 to b, but you might prefer to instatiate ?1 to a.
Auto Scroll to center cursor
With this option, Alfa tries to keep the cursor in the center of the window. With this option turned off, the part of the document you are working on might end up near the edge of the window, making it difficult to see what you are doing. With this option turned on, things might jump around too much.

[Menu bar image]

The Utils menu

[Utils menu image] These commands open (or close) auxiliary windows.