src/Pure/PIDE/protocol.scala
changeset 52527 dbac84eab3bc
parent 52111 1fd184eaa310
child 52530 99dd8b4ef3fe
--- a/src/Pure/PIDE/protocol.scala	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Jul 04 23:51:47 2013 +0200
@@ -17,7 +17,7 @@
       try {
         import XML.Decode._
         val body = YXML.parse_body(text)
-        Some(pair(long, list(pair(long, option(long))))(body))
+        Some(pair(long, list(pair(long, list(long))))(body))
       }
       catch {
         case ERROR(_) => None