removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;

enable search in pre-loaded theory;

more GUI options;

tuned signature;

tuned;

tuned GUI;

tuned name generation code (to make it easier to adapt later)

honor user type names if possible

merged;

more abstract consume_status operation;