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