src/Pure/PIDE/protocol.ML
changeset 47420 0dbe6c69eda2
parent 47404 e6e5750f1311
child 48707 ba531af91148
equal deleted inserted replaced
47419:c0e8c98ee50e 47420:0dbe6c69eda2
    48                     in Document.Header res end,
    48                     in Document.Header res end,
    49                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    49                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    50                   fn (a, []) => Document.Perspective (map int_atom a)]))
    50                   fn (a, []) => Document.Perspective (map int_atom a)]))
    51             end;
    51             end;
    52 
    52 
    53         val (assignment, state1) = Document.update old_id new_id edits state;
    53         val (assignment, state') = Document.update old_id new_id edits state;
    54         val _ =
    54         val _ =
    55           Output.protocol_message Isabelle_Markup.assign_execs
    55           Output.protocol_message Isabelle_Markup.assign_execs
    56             ((new_id, assignment) |>
    56             ((new_id, assignment) |>
    57               let open XML.Encode
    57               let open XML.Encode
    58               in pair int (list (pair int (option int))) end
    58               in pair int (list (pair int (option int))) end
    59               |> YXML.string_of_body);
    59               |> YXML.string_of_body);
    60         val state2 = Document.execute new_id state1;
    60 
    61       in state2 end));
    61         val _ = Document.start_execution state';
       
    62       in state' end));
    62 
    63 
    63 val _ =
    64 val _ =
    64   Isabelle_Process.protocol_command "Document.remove_versions"
    65   Isabelle_Process.protocol_command "Document.remove_versions"
    65     (fn [versions_yxml] => Document.change_state (fn state =>
    66     (fn [versions_yxml] => Document.change_state (fn state =>
    66       let
    67       let