src/Pure/PIDE/batch_session.scala
Sat, 18 Mar 2017 14:16:13 +0100 wenzelm actually throw exception;
less more (0) -10 -1 tip