changeset 52527 | dbac84eab3bc |
parent 52111 | 1fd184eaa310 |
child 52530 | 99dd8b4ef3fe |
--- a/src/Pure/PIDE/protocol.ML Thu Jul 04 16:04:53 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu Jul 04 23:51:47 2013 +0200 @@ -53,7 +53,7 @@ Output.protocol_message Markup.assign_execs ((new_id, assignment) |> let open XML.Encode - in pair int (list (pair int (option int))) end + in pair int (list (pair int (list int))) end |> YXML.string_of_body); val _ = List.app Future.cancel_group (Goal.reset_futures ());