less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
1.1 --- a/src/Pure/General/sha1.ML Thu Jul 24 10:22:34 2014 +0200
1.2 +++ b/src/Pure/General/sha1.ML Thu Jul 24 10:38:46 2014 +0200
1.3 @@ -10,6 +10,7 @@
1.4 eqtype digest
1.5 val digest: string -> digest
1.6 val rep: digest -> string
1.7 + val fake: string -> digest
1.8 end;
1.9
1.10 structure SHA1: SHA1 =
1.11 @@ -136,4 +137,6 @@
1.12 val digest = Digest o digest_string;
1.13 fun rep (Digest s) = s;
1.14
1.15 +val fake = Digest;
1.16 +
1.17 end;
2.1 --- a/src/Pure/General/sha1.scala Thu Jul 24 10:22:34 2014 +0200
2.2 +++ b/src/Pure/General/sha1.scala Thu Jul 24 10:38:46 2014 +0200
2.3 @@ -65,5 +65,7 @@
2.4 def digest(bytes: Bytes): Digest = bytes.sha1_digest
2.5
2.6 def digest(string: String): Digest = digest(Bytes(string))
2.7 +
2.8 + def fake(rep: String): Digest = new Digest(rep)
2.9 }
2.10
3.1 --- a/src/Pure/General/sha1_polyml.ML Thu Jul 24 10:22:34 2014 +0200
3.2 +++ b/src/Pure/General/sha1_polyml.ML Thu Jul 24 10:38:46 2014 +0200
3.3 @@ -46,4 +46,6 @@
3.4 val digest = Digest o digest_string;
3.5 fun rep (Digest s) = s;
3.6
3.7 +val fake = Digest;
3.8 +
3.9 end;
4.1 --- a/src/Pure/PIDE/document.ML Thu Jul 24 10:22:34 2014 +0200
4.2 +++ b/src/Pure/PIDE/document.ML Thu Jul 24 10:38:46 2014 +0200
4.3 @@ -296,12 +296,7 @@
4.4
4.5 fun define_blob digest text =
4.6 map_state (fn (versions, blobs, commands, execution) =>
4.7 - let
4.8 - val sha1_digest = SHA1.digest text;
4.9 - val _ =
4.10 - digest = SHA1.rep sha1_digest orelse
4.11 - error ("Ill-defined blob: bad SHA1 digest " ^ digest ^ " vs. " ^ SHA1.rep sha1_digest);
4.12 - val blobs' = Symtab.update (digest, (sha1_digest, split_lines text)) blobs;
4.13 + let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs
4.14 in (versions, blobs', commands, execution) end);
4.15
4.16 fun the_blob (State {blobs, ...}) digest =