src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Sun Apr 06 21:01:45 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 07 13:06:34 2014 +0200
@@ -18,7 +18,7 @@
   type state
   val init_state: state
   val define_blob: string -> string -> state -> state
-  type blob_digest = (string * string option) Exn.result
+  type blob_digest = (string * string * string option) Exn.result
   val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     state -> state
   val remove_versions: Document_ID.version list -> state -> state
@@ -219,7 +219,8 @@
 
 (** main state -- document structure and execution process **)
 
-type blob_digest = (string * string option) Exn.result;  (* file node name, raw digest*)
+type blob_digest =
+  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
@@ -291,6 +292,10 @@
     NONE => error ("Undefined blob: " ^ digest)
   | SOME content => content);
 
+fun resolve_blob state (blob_digest: blob_digest) =
+  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
+    (file, path, Option.map (the_blob state) raw_digest));
+
 
 (* commands *)
 
@@ -338,7 +343,7 @@
     val blobs' =
       (commands', Symtab.empty) |->
         Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
-          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+          fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
 
@@ -505,7 +510,7 @@
       val command_visible = visible_command node command_id';
       val command_overlays = overlays node command_id';
       val (command_name, blob_digests, span0) = the_command state command_id';
-      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blob_digests;
+      val blobs = map (resolve_blob state) blob_digests;
       val span = Lazy.force span0;
 
       val eval' =