edu.mit.csail.sdg.alloy4
Class ByteBuffer

java.lang.Object
  edu.mit.csail.sdg.alloy4.ByteBuffer

public final class ByteBuffer
extends java.lang.Object

Mutable; implements a growable array of bytes.

This class is more efficient than Java's ByteArrayOutputStream when writing large amount of data, because ByteArrayOutputStream will resize and copy entire existing contents every time the array needs to grow, whereas this class maintains a linked list of arrays (so when capacity is expanded we don't need to copy old data)

Constructor Summary

ByteBuffer()
Construct an empty byte buffer.

Method Summary

long	dump(java.io.RandomAccessFile os) Write the entire content into the given file as-is, then return the number of bytes written.
long	dumpFlate(java.io.RandomAccessFile os) Write the entire content into the given file using Flate compression (see RFC1951) then return the number of bytes written.
ByteBuffer	write(java.lang.String string) Write the given String into this byte buffer (by converting the String into its UTF-8 representation)
ByteBuffer	writes(double x) Write the given number into this byte buffer (truncated to the range -32767..+32767), followed by a space.
ByteBuffer	writes(long x) Write the given number into this byte buffer, followed by a space.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ByteBuffer

public ByteBuffer()

Construct an empty byte buffer.

Method Detail

write

public ByteBuffer write(java.lang.String string)

Write the given String into this byte buffer (by converting the String into its UTF-8 representation)

writes

public ByteBuffer writes(long x)

Write the given number into this byte buffer, followed by a space.

writes

public ByteBuffer writes(double x)

Write the given number into this byte buffer (truncated to the range -32767..+32767), followed by a space.

dumpFlate

public long dumpFlate(java.io.RandomAccessFile os)
               throws java.io.IOException

Write the entire content into the given file using Flate compression (see RFC1951) then return the number of bytes written.

Throws:

java.io.IOException

dump

public long dump(java.io.RandomAccessFile os)
          throws java.io.IOException

Write the entire content into the given file as-is, then return the number of bytes written.

Throws:

java.io.IOException