3.7 The window system

MacLogic includes a conventional window system, allowing the creation, opening, saving, and killing of windows. Some windows, like Derivation and Proof, are created for you: their contents can only be changed by using the formal systems, to ensure the logical correctness of their contents. Other windows (from the Jotter downwards in the Windows menu) can be edited freely: you can use them if you like for creating proofs, but MacLogic will not guarantee the correctness of proofs therein.

There is a window Advice, which contains (e.g.) some information about syntax. If you destroy its contents, you may need to restart MacLogic to get them back. If its presence annoys you, note that its visibility status can be stored in theSettings file: so close it, save the settings and then use those settings when you reload MacLogic.

Window names should be sensible, and may not conflict with file names: i.e. if you create a file it should not be given the same name as a window. (The file and window input/output work by reading to or from a channel, identified just by its name, hence obvious problems if names clash.)

Windows have "close boxes" at the top left corner: but they continue to be in memory after being closed, and can be re-opened again, usually by selection of the window's name in the Windows menu. Certain windows are part of the help system, and are only opened by selection of appropriate Help commands.

Text windows always appear in the Konstanz font. You can switch the size of the font between 9pt and 12 pt.

If you are a teacher using an LCD panel to show MacLogic to a class, you may find it convenient to put certain windows in bold face: use the Windows menu item Toggle bold.

The help system works by using five files ["ATP Help", "Syntax Help", "Menu Help", "Tactics Help" and "Rules Help"]. The first two are displayed directly; the last three are invisible, but extracts from them are displayed on request. Each of the files is loaded into memory when first needed; they are all killed if you invoke the command Help/Memory problems (of course, they can be loaded again if you wish).

Note that the dialogs are actually windows, of a different type: so, some of the commands that apply to windows, like editing commands, can be used on dialogs as well. One non-obvious feature of dialogs is that if you move a dialog, it should appear in the same place on the screen next time it is used: this is handy if you have a large screen. (Some dialogs, the "modal dialogs"---don't confuse this sense of "modal" with that in "modal logic"--- cannot be moved: they must be answered immediately.)