Wed, 31 Oct 2018 15:53:32 +0100 clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm [Wed, 31 Oct 2018 15:53:32 +0100] rev 69216
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
Wed, 31 Oct 2018 15:50:45 +0100 tuned;
wenzelm [Wed, 31 Oct 2018 15:50:45 +0100] rev 69215
tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 tip