Fixes for PG (Close 3763, 3770)

- Show does not print the goal twice
- Undo is considered as part of the document when PG mode
  (bug introduced when Undo was said not to be part of the document in
   coqtop mode).