less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;

--- a/src/Pure/General/sha1.ML	Thu Jul 24 10:22:34 2014 +0200
+++ b/src/Pure/General/sha1.ML	Thu Jul 24 10:38:46 2014 +0200
@@ -10,6 +10,7 @@
   eqtype digest
   val digest: string -> digest
   val rep: digest -> string
+  val fake: string -> digest
 end;
 
 structure SHA1: SHA1 =
@@ -136,4 +137,6 @@
 val digest = Digest o digest_string;
 fun rep (Digest s) = s;
 
+val fake = Digest;
+
 end;

--- a/src/Pure/General/sha1.scala	Thu Jul 24 10:22:34 2014 +0200
+++ b/src/Pure/General/sha1.scala	Thu Jul 24 10:38:46 2014 +0200
@@ -65,5 +65,7 @@
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
 
   def digest(string: String): Digest = digest(Bytes(string))
+
+  def fake(rep: String): Digest = new Digest(rep)
 }
 

--- a/src/Pure/General/sha1_polyml.ML	Thu Jul 24 10:22:34 2014 +0200
+++ b/src/Pure/General/sha1_polyml.ML	Thu Jul 24 10:38:46 2014 +0200
@@ -46,4 +46,6 @@
 val digest = Digest o digest_string;
 fun rep (Digest s) = s;
 
+val fake = Digest;
+
 end;

--- a/src/Pure/PIDE/document.ML	Thu Jul 24 10:22:34 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 24 10:38:46 2014 +0200
@@ -296,12 +296,7 @@
 
 fun define_blob digest text =
   map_state (fn (versions, blobs, commands, execution) =>
-    let
-      val sha1_digest = SHA1.digest text;
-      val _ =
-        digest = SHA1.rep sha1_digest orelse
-          error ("Ill-defined blob: bad SHA1 digest " ^ digest ^ " vs. " ^ SHA1.rep sha1_digest);
-      val blobs' = Symtab.update (digest, (sha1_digest, split_lines text)) blobs;
+    let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs
     in (versions, blobs', commands, execution) end);
 
 fun the_blob (State {blobs, ...}) digest =