proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;