method select_location loc = self#set_location (line_char_of_location file#buffer (Some loc)); file#select_location loc