GUI design
The most interesting part of Igloo's GUI is the proof window seen above. You can see how this is used in a series of screenshots, or read about it in my thesis.
Code layout
Igloo is a client/server style program. This is done to remove the need for end users to install the proof engine on their own machines. Communication between the client and server is achieved with TCP/IP sockets, using an XML based language designed for theorem proving interfaces named PGIP.
Communicator
The communicator module handles all data the travels between the client and the server.
Isabelle Server
The Isabelle Server is a small shell script wrapper for Isabelle. It listens for network connections, and once this is successful it spawns a copy of Isabelle and shovels data back and forth.
Mediator
This module is the main point of control for the system. When the communicator receives a message from the proof engine, it sends it to the mediator to decide what should be done with the message. The mediator may decide to update the display, ignore the message, or some other action. Events from the GUI call functions in the mediator, which then format a PGIP messages which are sent by the communicator to the proof engine.
GUI
The GUI is written in C++ using the wxWindows toolkit, a cross-platform library with targets for X11/Unix, Microsoft Windows, Macintosh (both OSX and earlier versions) as well as a few other obscure platforms. To see how the interface is used, see the screenshots of a sample proof in Igloo.