src/Pure/PIDE/protocol.ML
changeset 56458 a8d960baa5c2
parent 56447 1e77ed11f2f7
child 56616 abc2da18d08d
equal deleted inserted replaced
56457:eea4bbe15745 56458:a8d960baa5c2
    32       let
    32       let
    33         val blobs =
    33         val blobs =
    34           YXML.parse_body blobs_yxml |>
    34           YXML.parse_body blobs_yxml |>
    35             let open XML.Decode in
    35             let open XML.Decode in
    36               list (variant
    36               list (variant
    37                [fn ([], a) => Exn.Res (triple string string (option string) a),
    37                [fn ([], a) => Exn.Res (pair string (option string) a),
    38                 fn ([], a) => Exn.Exn (ERROR (string a))])
    38                 fn ([], a) => Exn.Exn (ERROR (string a))])
    39             end;
    39             end;
    40       in
    40       in
    41         Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
    41         Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
    42       end);
    42       end);