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

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