explicit type SHA1.digest;

--- a/src/Pure/General/sha1.ML	Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Pure/General/sha1.ML	Sun Mar 13 20:21:24 2011 +0100
@@ -7,7 +7,9 @@
 
 signature SHA1 =
 sig
-  val digest: string -> string
+  eqtype digest
+  val digest: string -> digest
+  val rep: digest -> string
 end;
 
 structure SHA1: SHA1 =
@@ -58,7 +60,7 @@
   in ((len + size padding) div 4, word) end;
 
 
-(* digest *)
+(* digest_string *)
 
 fun digest_word (i, w, {a, b, c, d, e}) =
   let
@@ -84,7 +86,7 @@
      e = d}
   end;
 
-fun digest str =
+fun digest_string str =
   let
     val (text_len, text) = padded_text str;
 
@@ -126,4 +128,12 @@
     val hex = hex_word o hash;
   in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end;
 
+
+(* type digest *)
+
+datatype digest = Digest of string;
+
+val digest = Digest o digest_string;
+fun rep (Digest s) = s;
+
 end;

--- a/src/Pure/General/sha1.scala	Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Pure/General/sha1.scala	Sun Mar 13 20:21:24 2011 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/sha1.scala
     Author:     Makarius
 
-Digesting strings according to SHA-1 (see RFC 3174).
+Digest strings according to SHA-1 (see RFC 3174).
 */
 
 package isabelle
@@ -12,7 +12,12 @@
 
 object SHA1
 {
-  def digest_bytes(bytes: Array[Byte]): String =
+  case class Digest(rep: String)
+  {
+    override def toString: String = rep
+  }
+
+  def digest_bytes(bytes: Array[Byte]): Digest =
   {
     val result = new StringBuilder
     for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
@@ -20,9 +25,9 @@
       if (i < 16) result += '0'
       result ++= Integer.toHexString(i)
     }
-    result.toString
+    Digest(result.toString)
   }
 
-  def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
+  def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s))
 }
 

--- a/src/Pure/General/sha1_polyml.ML	Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Pure/General/sha1_polyml.ML	Sun Mar 13 20:21:24 2011 +0100
@@ -9,6 +9,8 @@
 structure SHA1: SHA1 =
 struct
 
+(* digesting *)
+
 fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
 
 fun hex_string arr i =
@@ -28,8 +30,16 @@
         CInterface.POINTER (str, size str, CInterface.address digest);
   in fold (suffix o hex_string digest) (0 upto 19) "" end;
 
-fun digest str = digest_external str
+fun digest_string str = digest_external str
   handle CInterface.Foreign msg =>
-    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
+    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str));
+
+
+(* type digest *)
+
+datatype digest = Digest of string;
+
+val digest = Digest o digest_string;
+fun rep (Digest s) = s;
 
 end;

--- a/src/Pure/pure_setup.ML	Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Pure/pure_setup.ML	Sun Mar 13 20:21:24 2011 +0100
@@ -32,6 +32,7 @@
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
+toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";

--- a/src/Tools/cache_io.ML	Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Tools/cache_io.ML	Sun Mar 13 20:21:24 2011 +0100
@@ -67,7 +67,7 @@
     fun int_of_string s =
       (case read_int (raw_explode s) of
         (i, []) => i
-      | _ => err ())    
+      | _ => err ())
 
     fun split line =
       (case space_explode " " line of
@@ -80,7 +80,7 @@
         let val (key, l1, l2) = split line
         in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
       else ((i+1, l), tab)
-  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end 
+  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
 
 fun make path =
   let val table = if File.exists path then load path else (1, Symtab.empty)
@@ -98,7 +98,7 @@
   in {output=err, redirected_output=out, return_code=0} end
 
 fun lookup (Cache {path=cache_path, table}) str =
-  let val key = SHA1.digest str
+  let val key = SHA1.rep (SHA1.digest str)
   in
     (case Symtab.lookup (snd (Synchronized.value table)) key of
       NONE => (NONE, key)