wenzelm [Sun, 24 Jan 2016 12:21:57 +0100] rev 62234
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm [Sat, 23 Jan 2016 23:50:54 +0100] rev 62233
back to elementary options used in Isabelle2015 for jdk-7 -- none of the intermediate experiments for jdk-8 improved reactivity on particular dual-CPU system, but the problem seems to be absent on common single-CPU systems;