Source: utils/editor/edit_type_menu.pro
edit_type_menu Menu to select type of an edit. Usage: edit = edit_menu_type(times, group=group) Argument: times double input The JD range covered by the edit. Keyword: group long input The widget ID of a group leader, needed as this widget must be modal. History: Original: 15/2/01; SJT