src/Pure/Tools/print_operation.scala
Sat, 01 Apr 2017 19:17:15 +0200 wenzelm clarified YXML vs. symbol encoding: operate on whole message;
Tue, 14 Mar 2017 00:13:38 +0100 wenzelm tuned;
Tue, 14 Mar 2017 00:09:15 +0100 wenzelm misc tuning and simplification;
less more (0) -3 tip