Dynamic components/components with startup arguments

Isabelle is started with

isabelle logicname

where logicname is chosen from a list of heap images in the system/user's directory. The command

isatool findlogics

prints a list of the available heap images to the terminal. At the moment the existing interfaces each hard wire this command behind the scenes to refresh menus.

How can we do this kind of thing cleanly for PG Kit? Possibilities:

1. secondary process updating component configurations for broker -- ugly/compilicated
2. Isabelle itself doing same -- cleaner but a bit hacky
3. custom handling of component arguments similar to object mechanism -- can of worms

Any others? Perhaps 2 is the best option, although other provers may also have usefully adjustable startup parameters.

-- DavidAspinall - 29 Sep 2006

The broker already supports the updating of component configurations, i.e. we can add new components to a running broker. This supports (1) above very cleanly: to start Isabelle, we would start a compont which in essence calls "isaool findlogics", and sends the result back as a list of new component configurations, each corresponding to one instance of Isabelle. Then user can select which Isabelle logic they want (they'd appear as different provers in the prover startup menu offered by the display).

Some displays like PGEmacs or PGWin2 do not allow a prover startup menu, and just ask for a fixed prover to be run. That's fine as well, you just have to specify which Isabelle logic you want.

-- ChristophLueth - 29 Sep 2006

Aha, that's good. 1 is messy but maybe not so complicated. Probably this should be thought of as a non-problem for now.

Can we remove/replace components as well as add them?

-- DavidAspinall - 29 Sep 2006