src/Pure/PIDE/protocol_handlers.scala
2017-03-18 ago clarified signature;
2017-03-14 ago misc tuning and simplification;
2017-03-13 ago tuned signature;
2017-03-13 ago clarified modules;