src/Pure/Tools/print_operation.ML
Mon, 05 May 2014 15:17:07 +0200 wenzelm support print operations as asynchronous query;
less more (0) tip