# HG changeset patch
# User wenzelm
# Date 1384445877 -3600
# Node ID 2c4940d2edf7aebbac9dbdb269d541fc3dab64bf
# Parent  621a155c77150043f876b791aebc0cb5821416d2
tuned signature;

diff -r 621a155c7715 -r 2c4940d2edf7 src/Pure/General/bytes.scala
--- 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)
 }
 
diff -r 621a155c7715 -r 2c4940d2edf7 src/Pure/General/file.scala
--- 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)
 
 
diff -r 621a155c7715 -r 2c4940d2edf7 src/Pure/General/sha1.scala
--- 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))
 }
 
diff -r 621a155c7715 -r 2c4940d2edf7 src/Pure/System/isabelle_process.scala
--- 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 =
diff -r 621a155c7715 -r 2c4940d2edf7 src/Pure/System/utf8.scala
--- 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 */