src/Pure/PIDE/command.ML
changeset 55893 cee77d2e9582
parent 55892 5fed81762406
child 55896 11087efad95e
     1.1 --- a/src/Pure/PIDE/command.ML	Tue Nov 19 19:33:27 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Nov 19 19:43:26 2013 +0100
     1.3 @@ -89,9 +89,9 @@
     1.4    (case Thy_Syntax.parse_spans toks of
     1.5      [span] => span
     1.6        |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
     1.7 -        blobs |> map (Exn.release #> (fn (file, text) =>
     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 +          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
    1.12        |> Thy_Syntax.span_content
    1.13    | _ => toks);
    1.14