src/Pure/PIDE/protocol.ML
changeset 59714 ae322325adbb
parent 59685 c043306d2598
child 59715 4f0d0e4ad68d
--- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:30:54 2015 +0100
@@ -32,11 +32,15 @@
       let
         val (blobs, blobs_index) =
           YXML.parse_body blobs_yxml |>
-            let open XML.Decode in
+            let
+              val message =
+                YXML.string_of_body o Protocol_Message.command_positions id;
+              open XML.Decode;
+            in
               pair
                 (list (variant
                  [fn ([], a) => Exn.Res (pair string (option string) a),
-                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+                  fn ([], a) => Exn.Exn (ERROR (message a))]))
                 int
             end;
         val toks =