src/Pure/PIDE/document.ML
changeset 56447 1e77ed11f2f7
parent 56208 06cc31dff138
child 56458 a8d960baa5c2
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Apr 06 21:01:45 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 07 13:06:34 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val define_blob: string -> string -> state -> state
     1.7 -  type blob_digest = (string * string option) Exn.result
     1.8 +  type blob_digest = (string * string * string option) Exn.result
     1.9    val define_command: Document_ID.command -> string -> blob_digest list -> string ->
    1.10      state -> state
    1.11    val remove_versions: Document_ID.version list -> state -> state
    1.12 @@ -219,7 +219,8 @@
    1.13  
    1.14  (** main state -- document structure and execution process **)
    1.15  
    1.16 -type blob_digest = (string * string option) Exn.result;  (* file node name, raw digest*)
    1.17 +type blob_digest =
    1.18 +  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
    1.19  
    1.20  type execution =
    1.21   {version_id: Document_ID.version,  (*static version id*)
    1.22 @@ -291,6 +292,10 @@
    1.23      NONE => error ("Undefined blob: " ^ digest)
    1.24    | SOME content => content);
    1.25  
    1.26 +fun resolve_blob state (blob_digest: blob_digest) =
    1.27 +  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
    1.28 +    (file, path, Option.map (the_blob state) raw_digest));
    1.29 +
    1.30  
    1.31  (* commands *)
    1.32  
    1.33 @@ -338,7 +343,7 @@
    1.34      val blobs' =
    1.35        (commands', Symtab.empty) |->
    1.36          Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    1.37 -          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    1.38 +          fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    1.39  
    1.40    in (versions', blobs', commands', execution) end);
    1.41  
    1.42 @@ -505,7 +510,7 @@
    1.43        val command_visible = visible_command node command_id';
    1.44        val command_overlays = overlays node command_id';
    1.45        val (command_name, blob_digests, span0) = the_command state command_id';
    1.46 -      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blob_digests;
    1.47 +      val blobs = map (resolve_blob state) blob_digests;
    1.48        val span = Lazy.force span0;
    1.49  
    1.50        val eval' =