src/Pure/PIDE/protocol.ML
changeset 59714 ae322325adbb
parent 59685 c043306d2598
child 59715 4f0d0e4ad68d
     1.1 --- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:07:56 2015 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:30:54 2015 +0100
     1.3 @@ -32,11 +32,15 @@
     1.4        let
     1.5          val (blobs, blobs_index) =
     1.6            YXML.parse_body blobs_yxml |>
     1.7 -            let open XML.Decode in
     1.8 +            let
     1.9 +              val message =
    1.10 +                YXML.string_of_body o Protocol_Message.command_positions id;
    1.11 +              open XML.Decode;
    1.12 +            in
    1.13                pair
    1.14                  (list (variant
    1.15                   [fn ([], a) => Exn.Res (pair string (option string) a),
    1.16 -                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
    1.17 +                  fn ([], a) => Exn.Exn (ERROR (message a))]))
    1.18                  int
    1.19              end;
    1.20          val toks =