[toplevel] Modify printing goal strategy.

Instead of using a command-analysis heuristic, coqtop will now print
goals if the goal has changed. We use a fast goal comparison
heuristic, but a more refined strategy would be possible.

This brings some [IMHO very welcome] change to PG and `-emacs`, which
will now disable the printing of goals. Now, instead of playing with
`Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show`
command whenever it wishes to redisplay the goals.

This change will break PG, so we need to carefully coordinate this PR
with PG upstream (see ProofGeneral/PG#212).

Some interesting further things to do:

- Detect changes in nested proofs.
- Uncouple the silent flag from "print goals".

0 files changed, 0 insertions, 0 deletions