src/Pure/PIDE/command.ML
changeset 54520 cee77d2e9582
parent 54519 5fed81762406
child 54523 11087efad95e
--- a/src/Pure/PIDE/command.ML	Tue Nov 19 19:33:27 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Nov 19 19:43:26 2013 +0100
@@ -89,9 +89,9 @@
   (case Thy_Syntax.parse_spans toks of
     [span] => span
       |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
-        blobs |> map (Exn.release #> (fn (file, text) =>
+        blobs |> (map o Exn.map_result) (fn (file, text) =>
           let val _ = Position.report pos (Markup.path file);
-          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end)))
+          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
       |> Thy_Syntax.span_content
   | _ => toks);