src/Pure/PIDE/document.ML
changeset 57638 ed58e740a699
parent 57616 50ab1db5c0fd
child 57643 858bee39acde
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 24 10:22:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 24 10:38:46 2014 +0200
     1.3 @@ -296,12 +296,7 @@
     1.4  
     1.5  fun define_blob digest text =
     1.6    map_state (fn (versions, blobs, commands, execution) =>
     1.7 -    let
     1.8 -      val sha1_digest = SHA1.digest text;
     1.9 -      val _ =
    1.10 -        digest = SHA1.rep sha1_digest orelse
    1.11 -          error ("Ill-defined blob: bad SHA1 digest " ^ digest ^ " vs. " ^ SHA1.rep sha1_digest);
    1.12 -      val blobs' = Symtab.update (digest, (sha1_digest, split_lines text)) blobs;
    1.13 +    let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs
    1.14      in (versions, blobs', commands, execution) end);
    1.15  
    1.16  fun the_blob (State {blobs, ...}) digest =