Sun, 20 Jun 2004 09:27:32 +0200 wenzelm added escape, export encode_raw, default mode now trivial, tuned;
Sun, 20 Jun 2004 09:27:24 +0200 wenzelm use_output: Symbol.escape;
Sun, 20 Jun 2004 09:27:17 +0200 wenzelm tuned pp;
Sun, 20 Jun 2004 09:27:04 +0200 wenzelm avoid premature evaluation of syn_of (wastes time in conjunction with pp);
Sun, 20 Jun 2004 09:26:48 +0200 wenzelm Symbol.encode_raw;
Sun, 20 Jun 2004 09:26:29 +0200 wenzelm tuned;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip