Forbid suggestions on non-public declarations

Author: robsimmons

src/Lean/IdentifierSuggestion.lean

@@ -47,6 +47,8 @@ builtin_initialize identifierSuggestionForAttr : PersistentEnvExtension
         | -- Attributes parsed _before the suggest_for notation is added
           .node _ ``Parser.Attr.simple #[.ident _ _ `suggest_for [], .node _ `null #[id]] => pure #[id]
         | _ => throwError "Invalid `[suggest_for]` attribute syntax {repr stx}"
+      if isPrivateName decl then
+        throwError "Cannot make suggestions for private names"
       modifyEnv (ext.addEntry · (decl, altSyntaxIds.map (·.getId)))
   }
 

tests/pkg/module/Module/Basic.lean

@@ -510,3 +510,17 @@ public meta def delab : Lean.PrettyPrinter.Delaborator.Delab :=
 
 public def noMetaDelab : Lean.PrettyPrinter.Delaborator.Delab :=
   default
+
+/-- error: Cannot make suggestions for private names -/
+#guard_msgs in
+@[suggest_for Bar1]
+def FooBar1 := 4
+
+/-- error: Cannot make suggestions for private names -/
+#guard_msgs in
+@[suggest_for Bar2]
+meta def FooBar2 := 4
+
+#guard_msgs in
+@[suggest_for Bar3 FooBar1 FooBar2]
+public def FooBar3 := 4