translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases

adding size as static argument in quickcheck_narrowing compilation

modernized specifications;

dropped unused structure aliases;

tuned;

NEWS: structure Timing provides various operations for timing;

simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);

pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;

structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;

pervasive cond_timeit;