// FIXME What we'd really like to do is to be able to output some
// appropriate sort of text here. But to do that, we need to associate
// some sort of counter with the label, and we don't have that yet.
// FIXME What we'd really like to do is to be able to output some
// appropriate sort of text here. But to do that, we need to associate
// some sort of counter with the label, and we don't have that yet.