src/Pure/PIDE/protocol.ML
changeset 70469 3e17c3a5fd39
parent 70030 09f200c658ed
child 70853 4a358f8c7cb7
     1.1 --- a/src/Pure/PIDE/protocol.ML	Sun May 19 14:14:56 2019 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Sun May 19 18:10:45 2019 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  
     1.5              val _ = Execution.discontinue ();
     1.6  
     1.7 -            val (removed, assign_update, state') =
     1.8 +            val (edited, removed, assign_update, state') =
     1.9                Document.update old_id new_id edits consolidate state;
    1.10              val _ =
    1.11                (singleton o Future.forks)
    1.12 @@ -117,12 +117,12 @@
    1.13  
    1.14              val _ =
    1.15                Output.protocol_message Markup.assign_update
    1.16 -                ((new_id, assign_update) |>
    1.17 +                ((new_id, edited, assign_update) |>
    1.18                    let
    1.19                      open XML.Encode;
    1.20                      fun encode_upd (a, bs) =
    1.21                        string (space_implode "," (map Value.print_int (a :: bs)));
    1.22 -                  in pair int (list encode_upd) end
    1.23 +                  in triple int (list string) (list encode_upd) end
    1.24                    |> YXML.chunks_of_body);
    1.25            in Document.start_execution state' end)));
    1.26