HomeIsabelle/Phabricator

clarified messages, depending on option "document_echo";