get_read_names
-io io_handle:integer
?identifier ...?
This command converts a list of reading identifiers to reading names. The identifiers can be either "#number" or the actual read name itself, although the command is obviously only useful for the first syntax. The names are returned as a Tcl list.