src/Pure/General/output_primitives.ML
Sat, 18 Mar 2017 12:46:52 +0100 wenzelm restore output channels after shutdown, e.g. relevant for saved heap;
Sat, 09 Apr 2016 19:38:25 +0200 wenzelm proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
Sat, 09 Apr 2016 16:16:05 +0200 wenzelm shared output primitives of physical/virtual Pure;
less more (0) tip