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

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 29 Sep 2006 - 10:11:53 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies