Add features: use goal count information printed at top of goals buffer in modeline, clear the goal window when proof is skipped (abort, admitted...).#755