src/Pure/PIDE/protocol.ML
changeset 50201 c26369c9eda6
parent 49931 85780e6f8fd2
child 50498 6647ba2775c1
equal deleted inserted replaced
50200:2c94c065564e 50201:c26369c9eda6
    51                   fn (a, []) => Document.Perspective (map int_atom a)]))
    51                   fn (a, []) => Document.Perspective (map int_atom a)]))
    52             end;
    52             end;
    53 
    53 
    54         val (assignment, state') = Document.update old_id new_id edits state;
    54         val (assignment, state') = Document.update old_id new_id edits state;
    55         val _ =
    55         val _ =
    56           Output.protocol_message Isabelle_Markup.assign_execs
    56           Output.protocol_message Markup.assign_execs
    57             ((new_id, assignment) |>
    57             ((new_id, assignment) |>
    58               let open XML.Encode
    58               let open XML.Encode
    59               in pair int (list (pair int (option int))) end
    59               in pair int (list (pair int (option int))) end
    60               |> YXML.string_of_body);
    60               |> YXML.string_of_body);
    61 
    61 
    70       let
    70       let
    71         val versions =
    71         val versions =
    72           YXML.parse_body versions_yxml |>
    72           YXML.parse_body versions_yxml |>
    73             let open XML.Decode in list int end;
    73             let open XML.Decode in list int end;
    74         val state1 = Document.remove_versions versions state;
    74         val state1 = Document.remove_versions versions state;
    75         val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
    75         val _ = Output.protocol_message Markup.removed_versions versions_yxml;
    76       in state1 end));
    76       in state1 end));
    77 
    77 
    78 val _ =
    78 val _ =
    79   Isabelle_Process.protocol_command "Document.invoke_scala"
    79   Isabelle_Process.protocol_command "Document.invoke_scala"
    80     (fn [id, tag, res] =>
    80     (fn [id, tag, res] =>