fix(util/name): escape empty name components using french quotes

src/frontends/lean/pp.cpp

@@ -1842,7 +1842,7 @@ std::string sexpr_to_string(sexpr const & s) {
 // check whether a space must be inserted between the strings so that lexing them would
 // produce separate tokens
 std::pair<bool, token_table const *> pretty_fn::needs_space_sep(token_table const * last, std::string const & s1, std::string const & s2) const {
-    if (is_id_rest(get_utf8_last_char(s1.data()), s1.data() + s1.size()) && is_id_rest(s2.data(), s2.data() + s2.size()))
+    if (s1.size() == 0 || (is_id_rest(get_utf8_last_char(s1.data()), s1.data() + s1.size()) && is_id_rest(s2.data(), s2.data() + s2.size())))
         return mk_pair(true, nullptr); // would be lexed as a single identifier without space
 
     if (last) {

src/util/name.cpp

@@ -75,7 +75,7 @@ void name::imp::display_core(std::ostream & out, imp * p, bool escape, char cons
                 }
             }
         }
-        if (must_escape)
+        if (must_escape || sz == 0)
             out << "«" << p->m_str << "»";
         else
             out << p->m_str;

tests/lean/empty_french_quote.lean

@@ -0,0 +1,4 @@
+def «» := not
+theorem thm : «» false := id
+#print «»
+#print thm

tests/lean/empty_french_quote.lean.expected.out

@@ -0,0 +1,4 @@
+def «» : Prop → Prop :=
+not
+theorem thm : «» false :=
+id