1.1 --- a/src/Pure/PIDE/command.ML	Tue Nov 19 20:59:05 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Nov 19 21:49:31 2013 +0100
     1.3 @@ -88,10 +88,20 @@
     1.4  fun resolve_files blobs toks =
     1.5    (case Thy_Syntax.parse_spans toks of
     1.6      [span] => span
     1.7 -      |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
     1.8 -        blobs |> (map o Exn.map_result) (fn (file, text) =>
     1.9 -          let val _ = Position.report pos (Markup.path file);
    1.10 -          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
    1.11 +      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    1.12 +        let
    1.13 +          fun make_file src_path (Exn.Res (file, text)) =
    1.14 +                let val _ = Position.report pos (Markup.path file);
    1.15 +                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
    1.16 +            | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.17 +
    1.18 +          val src_paths = Keyword.command_files cmd path;
    1.19 +        in
    1.20 +          if null blobs then []
    1.21 +          else if length src_paths <> length blobs then
    1.22 +            error ("Misalignment of inlined files" ^ Position.here pos)
    1.23 +          else map2 make_file src_paths blobs
    1.24 +        end)
    1.25        |> Thy_Syntax.span_content
    1.26    | _ => toks);
    1.27