--- a/src/Pure/General/bytes.scala Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/General/bytes.scala Thu Nov 14 17:17:57 2013 +0100
@@ -8,6 +8,9 @@
package isabelle
+import java.io.{File => JFile, OutputStream, FileInputStream}
+
+
object Bytes
{
val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
@@ -17,10 +20,32 @@
val str = s.toString
if (str.isEmpty) empty
else {
- val bytes = UTF8.string_bytes(str)
+ val bytes = str.getBytes(UTF8.charset)
new Bytes(bytes, 0, bytes.length)
}
}
+
+
+ /* read */
+
+ def read(file: JFile): Bytes =
+ {
+ var i = 0
+ var m = 0
+ val n = file.length.toInt
+ val bytes = new Array[Byte](n)
+
+ val stream = new FileInputStream(file)
+ try {
+ do {
+ m = stream.read(bytes, i, n - i)
+ if (m != -1) i += m
+ } while (m != -1 && n > i)
+ }
+ finally { stream.close }
+
+ new Bytes(bytes, 0, bytes.length)
+ }
}
final class Bytes private(
@@ -30,6 +55,17 @@
{
/* equality */
+ override def equals(that: Any): Boolean =
+ {
+ that match {
+ case other: Bytes =>
+ if (this eq other) true
+ else if (length != other.length) false
+ else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
+ case _ => false
+ }
+ }
+
private lazy val hash: Int =
{
var h = 0
@@ -42,32 +78,28 @@
override def hashCode(): Int = hash
- override def equals(that: Any): Boolean =
- {
- that match {
- case other: Bytes =>
- if (this eq other) true
- else if (length != other.length) false
- else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
- case _ => false
- }
- }
-
/* content */
+ def sha1_digest: SHA1.Digest = SHA1.digest(bytes)
+
override def toString: String = new String(bytes, offset, length, UTF8.charset)
- def is_empty: Boolean = length == 0
+ def isEmpty: Boolean = length == 0
def +(other: Bytes): Bytes =
- if (other.is_empty) this
- else if (is_empty) other
+ if (other.isEmpty) this
+ else if (isEmpty) other
else {
val new_bytes = new Array[Byte](length + other.length)
java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
new Bytes(new_bytes, 0, new_bytes.length)
}
+
+
+ /* write */
+
+ def write(stream: OutputStream): Unit = stream.write(bytes, offset, length)
}
--- a/src/Pure/General/file.scala Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/General/file.scala Thu Nov 14 17:17:57 2013 +0100
@@ -36,25 +36,7 @@
/* read */
- def read_bytes(file: JFile): Array[Byte] =
- {
- var i = 0
- var m = 0
- val n = file.length.toInt
- val buf = new Array[Byte](n)
-
- val stream = new FileInputStream(file)
- try {
- do {
- m = stream.read(buf, i, n - i)
- if (m != -1) i += m
- } while (m != -1 && n > i)
- }
- finally { stream.close }
- buf
- }
-
- def read(file: JFile): String = new String(read_bytes(file), UTF8.charset)
+ def read(file: JFile): String = Bytes.read(file).toString
def read(path: Path): String = read(path.file)
--- a/src/Pure/General/sha1.scala Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/General/sha1.scala Thu Nov 14 17:17:57 2013 +0100
@@ -56,6 +56,8 @@
make_result(digest)
}
- def digest(string: String): Digest = digest(UTF8.string_bytes(string))
+ def digest(bytes: Bytes): Digest = bytes.sha1_digest
+
+ def digest(string: String): Digest = digest(Bytes(string))
}
--- a/src/Pure/System/isabelle_process.scala Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Nov 14 17:17:57 2013 +0100
@@ -110,7 +110,7 @@
/* command input actor */
- private case class Input_Chunks(chunks: List[Array[Byte]])
+ private case class Input_Chunks(chunks: List[Bytes])
private case object Close
private def close(p: (Thread, Actor))
@@ -261,8 +261,8 @@
//{{{
receive {
case Input_Chunks(chunks) =>
- stream.write(UTF8.string_bytes(chunks.map(_.length).mkString("", ",", "\n")))
- chunks.foreach(stream.write(_))
+ Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
+ chunks.foreach(_.write(stream))
stream.flush
case Close =>
stream.close
@@ -362,13 +362,13 @@
/** main methods **/
- def protocol_command_raw(name: String, args: Array[Byte]*): Unit =
- command_input._2 ! Input_Chunks(UTF8.string_bytes(name) :: args.toList)
+ def protocol_command_raw(name: String, args: Bytes*): Unit =
+ command_input._2 ! Input_Chunks(Bytes(name) :: args.toList)
def protocol_command(name: String, args: String*)
{
receiver(new Input(name, args.toList))
- protocol_command_raw(name, args.map(UTF8.string_bytes): _*)
+ protocol_command_raw(name, args.map(Bytes(_)): _*)
}
def options(opts: Options): Unit =
--- a/src/Pure/System/utf8.scala Thu Nov 14 16:55:32 2013 +0100
+++ b/src/Pure/System/utf8.scala Thu Nov 14 17:17:57 2013 +0100
@@ -20,8 +20,6 @@
val charset: Charset = Charset.forName(charset_name)
def codec(): Codec = Codec(charset)
- def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
-
/* permissive UTF-8 decoding */