src/Pure/PIDE/protocol_message.ML
2015-03-16 ago tuned protocol -- resolve command positions in ML;