src/Pure/System/invoke_scala.ML
Sat, 02 Nov 2019 12:02:27 +0100 wenzelm more scalable protocol_message: use XML.body directly (Output.output hook is not required);
less more (0) -10 -1 tip