Legend:
Library
Module
Module type
Parameter
Class
Class type
module Item : sig ... end

A widget for selecting multiple items from a list. A fairly rich interface is provided, including:

  • Using the arrow keys and Enter to select / deselect items;
  • The ability to filter the set of items displayed by searching;
  • "Select all" and "Select none" buttons
module View_config : sig ... end
module Selection_status : sig ... end
module Action : sig ... end
module Result : sig ... end
module Initial_model_settings : sig ... end