public interface TokenPusher
An object capable of transferring a token from a random-access
source to a target. A
TokenPusher only exists in the
context of a source and target. The source is normally a
TokenSequence, the target an output port.
Using a TokenPusher provides an efficient way for copying
tokens one at a time, without requiring constant type checks.
An example of this would be reading some number of tokens from an input,
sorting them with a TokenSorter, and then pushing them on an output
in sorted order:
TokenArrayWriter buffer= TokenArrays.allocateWriter(input.getType(), size);
input.transfer(buffer, size);
int[] ordering= TokenSorter.MERGE_SORT.sort(buffer);
TokenPusher pusher= PortTokenUtilities.constructPusher(output, buffer);
for (int index : ordering) pusher.push(index);
-
Method Summary
Modifier and TypeMethodDescriptionvoidpush(int index) Pushes the specified token from the source to the target.
-
Method Details
-
push
void push(int index) Pushes the specified token from the source to the target.- Parameters:
index- the token to push
-