[toplevel] Restore 8.6 goal printing behavior.

When porting the toplevel to the STM, the logic for goal printing was
simplified too much under optimistic assumptions. The idea was not to
rely on the `vernac_classifier` which is an internal and complicated
beast.

However, it seems there are many cases to consider other than
`is_query`, so at the risk of reimplementing the classifier we revert
to the old approach of using the full classification.

This gives maximum 8.6 compatibility, with the pitfall of having to
call the classifier. Indeed, due to the dynamic nature of the "undo
classifier", we cannot call it after `Stm.add`, as the document tree
will be not the right one, making the classification of undo commands
incorrect (actually raising an error "Cannot undo").

0 files changed, 0 insertions, 0 deletions