src/Pure/PIDE/protocol.ML
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 ());