fix: ignore syntactically incorrect commands that do not contain any symbol

This kind of broken command does not have a position information, and
was producing a panic message in the server because it makes the
reasonable assumption that every command returned by `parserCommand`
has a position.

src/Lean/Parser/Module.lean

@@ -89,7 +89,10 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext)
         -- advance at least one token to prevent infinite loops
         let pos := if s.pos == pos then consumeInput c s.pos else s.pos
         let messages := if recovering && s.stxStack.isEmpty then messages else messages.add <| mkErrorMessage c s.pos (toString errorMsg)
-        if s.stxStack.isEmpty then
+        /- We ignore commands where `getPos?` is none. This happens only on commands that have a prefix comprised of optional elements.
+           For example, unification hints start with `optional («scoped» <|> «local»)`.
+           We claim a syntatically incorrect command containing no token or identifier is irrelevant for intellisense and should be ignored. -/
+        if s.stxStack.isEmpty || s.stxStack.back.getPos?.isNone then
           parse { pos := pos, recovering := true } messages
         else
           (s.stxStack.back, { pos := pos, recovering := true }, messages)