src/Pure/PIDE/document.ML
changeset 61077 06cca32aa519
parent 60937 51425cbe8ce9
child 62505 9e2a65912111
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Sep 01 22:32:58 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Sep 01 23:10:23 2015 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4    | SOME content => content);
     1.5  
     1.6  fun resolve_blob state (blob_digest: blob_digest) =
     1.7 -  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
     1.8 +  blob_digest |> Exn.map_res (fn (file_node, raw_digest) =>
     1.9      (file_node, Option.map (the_blob state) raw_digest));
    1.10  
    1.11  fun blob_reports pos (blob_digest: blob_digest) =