The extended generic interface technology consists of two main layers:

1. GenGUI

GenGUI handles _items_ (which can be leaf items or folder items
containing other items). Items do not have a notion of state, and are
described by class CItem. 

GenGUI provides a big widget containing three subwidgets A, B and C:

	  +------+---------+
	  |      |         |
	  |  A   |         |
	  +------+    C    |
	  |      |         |
	  |  B   |         |
	  +------+---------+

where A is a tree widget which contains the folder items
      B is the _notepad_ containing leaf items
      C is a multi-purpose widget, which can be used as the
        construction area (see below)

This should be configurable, i.e. one should be able to place A and B
side by side and C below etc. Also nice would be panes which allow the
borders to be moved, but Tk can't do that. 

2. xgit (formerly known as GenIT)

xgit constructs typed objects by apply operations which are implemented
using tools.

2.1. Types

The types determine the icon of the object, plus via the arities the
applicable operations. Types can be construction types, which means
that operations are only applicable when the object is open in the
construction area. Thus, we have

> data ObjType = ObjType String Icon Bool

2.2 Objects

Objects have a value (possibly-- they can become outdated), and are
constructed using operations. xgit keeps track of how they are
constructed. 

We distinguish between external and internal objects.

External objects are primarily files (but also files on a CVS or ftp
server etc.)

Internal objects only exist inside the tool. They are displayed using
the tool, and come in three kinds:

- basic objects: Things like theorems or theories which are given by
  an identifier ("HOL.trans"). They may depend on an external object
  (not only for outdating, but moreover for reconstructing the object state).

- derived objects: given by applying a single command, e.g.
  th1 RS th2 or (more complicatedly) a theorem derived from a proof
  with "qed". 

- constructed objects: given by applying a sequence of commands. Prime
  example: proofs. 

The difference between derived and constructed objects is that with
the latter, the first argument of the commands is (implicitly) the
object under construction. 

The actual type of object values is given by the tool, and hence xgit
is polymorph over the object value:

> class ObjVal v where
>   display :: v -> IO MarkupText

> data ObjVal v=> Obj v = 
>   BasicObj   { type :: ObjType, val :: Variable (Maybe v), 
                 id  :: Id, ext :: Maybe ExtObj }
> | DerivedObj { type :: ObjType, val :: Variable (Maybe v), cmd :: Cmd }
> | ConstrObj  { type :: ObjType, val :: Variable (Maybe v), cmds :: [Cmd] }

The identifier is just a string:

> newtype Id  = Id String

A command is given by a list of objects -- the arguments of the
command -- and a tool command (which is just a string to be sent to
the tool. The string already has the argument(s) substituted at the
appropriate places; the objects are just there to keep track of
dependencies. 
 
> type Cmd = ([Obj], Cmdline) 

depends :: Obj -> [Obj] 
depends (BasicObj _)                 = [] 
depends (DerivedObj{cmd= (objs, _)}) = objs
depends (ConstrObj{cmds= (objs, _)}) = concat objs

An external object is a file. External objects contain definitions,
proof scripts, theories, specifications and must be loaded into the
tool in order to be able to access a basic object. They are not
displayed directly, since they cannot be edited from within the tool,
and have no direct use. (Not too sure about this-- may in fact want
ExtObj to be an object variant.)

In the following, the name is used when displaying the object (to the
user), the id is the identification to the tool, and the uri is the
precise location of the thing. (We only need to provide the URI, and
it then calculates the rest for us.)

> data ExtObj = ExtObj { name :: Name,
>                        uri  :: URI,
>                        id   :: String,
>                        type :: ObjType }

The object type is merely used to indicate what type of objects are in
this theory. Here's an example: an Isabelle theory
might be known as 

ExtObj{name= "HOL", 
       uri = "file:/home/cxl/src/HOL.thy", 
       id  = "HOL.thy",
       type = isaTheory}

2.3 Commands 

A commandline is a string sent to the tool. Commandlines are given as
operations (see below), or directly as strings. 

newtype Cmdline = Cmdline String

Hence, there should be a text entry box which allows direct input of
commands. If we drag&drop basic objects into this text box, their ids
are inserted at the current cursor position; if we drop derived or
constructed objects into it, their commands will be inserted. Once a
text entry is finished, it will be parsed for dependencies-- see Tool
class below, method cmdDep; the Ids returned are the basic objects
this command (and hence the constructed object it constructs) depend
on. 


2.4 Operations

Operations correspond to a command sent to a tool, where it gets
evaluated to produce new objects (or an error). 

An operation has an arity, just like in many-sorted algebra, which
consists of a list of argument types and a single target type. 

(Note our lists are slightly funny, to accomodate Isabelle-style "list
 types"-- a single type which designates a list of objects of that
 type, like the arguments of rtac.)

> data Opn = Opn (OList ObjType)  -- source
>                ObjType          -- target
>                ([Obj]-> Cmd)    -- the command
>
> data OList a = OMt
>              | OCons a (OList a)
>              | OSgl  a


2.5 The Tool

The tool gets sent a command, and produces a response. It is also used
to display object values, and load external objects. 

>class Tool t where
>   start  :: IO t       -- start tool
>   stop   :: t-> IO ()  -- stop tool
>   break  :: t-> IO ()  -- send interrupt
>
>   display :: ObjVal v=> t -> v-> IO MarkupText
>
>   send    :: ObjVal v=> t-> Cmd v-> IO (Response v)
>   load    :: t-> ExtObj-> IO (Response [Id])
>
>   cmdDep  :: t-> Cmdline-> IO [Id]
>
>data ObjVal v=> Response v= Either MarkupText v

The PGWin tool is an instantiation of the generic tool for a PGWin
prover.

Commands				Answers

- apply tactic				- new proofstate (or failure)
- apply command (e.g. RS)		- new value (or failure)
- display theorem, or other value	- value
- find/list theorems/theories		- list of ids
- read file/external object		- list of ids, or error

Note that different PGWin tools will still have different types and
operations, e.g. IsaWin vs. TAS.

2.6 The export interface

New tools can only be added at compile time to xgit-- so xgit is
generic over the tools.  

The types, operations and objects xgit knows about, together with
visual layout such as menus and buttons, form the _configuration_. The
configuration can be changed at runtime -- so users can add operations
and buttons -- within certain limits. For example, we can add a new
operation by giving its arity, and supplying a command line for it;
and we can add new buttons or menu entries which trigger operations.

The OList type is visible; the 
data OList a = ... -- see above

data ObjType
newType :: String -> Icon-> Bool-> IO ObjType

data Opn
newOpn  :: OList ObjType-> ObjType-> Toolcmd-> IO Opn

data Toolcmd
cmd :: String-> Toolcmd

-- these add a (unary!) operation to the menu/as a shortcut button to
-- the con/area.
newMenuOp :: Opn-> String-> IO ()
newButtonOp :: Opn -> Bitmap ?? -> IO ()
-- then again, we could just export
applyOpn :: Opn-> ... -> IO ()
-- which would apply an operation

data ExtObj 
newExtObj :: URI-> ObjType-> IO ExtObj

-- object construction