src/Pure/PIDE/protocol.ML

--- a/src/Pure/PIDE/protocol.ML	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Nov 20 11:55:52 2013 +0100
@@ -34,8 +34,8 @@
           YXML.parse_body blobs_yxml |>
             let open XML.Decode in
               list (variant
-               [fn ([a, b], []) => Exn.Res (a, b),
-                fn ([a], []) => Exn.Exn (ERROR a)])
+               [fn ([], a) => Exn.Res (pair string (option string) a),
+                fn ([], a) => Exn.Exn (ERROR (string a))])
             end;
       in
         Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)