fix: import completion after meta import (#8704)

The details of `identWithPartialTrailingDot` prevent a robust approach
using quotations.

Author: Kha

src/Lean/Server/Completion/ImportCompletion.lean

@@ -24,15 +24,18 @@ def AvailableImports.toImportTrie (imports : AvailableImports) : ImportTrie := I
     importTrie := importTrie.insert i i
   return importTrie
 
-/-- Checks whether `completionPos` points at the position after an incomplete `import` statement. -/
 def isImportNameCompletionRequest (headerStx : TSyntax ``Parser.Module.header) (completionPos : String.Pos) : Bool := Id.run do
   let `(Parser.Module.header| $[module]? $[prelude]? $importsStx*) := headerStx
     | return false
-  importsStx.anyM fun
-    | `(Parser.Module.import| $[private]? $[meta]? import%$importCmd $[all%$allTk?]? $importId) =>
-      let keywordsTailPos := allTk?.bind (·.getTailPos?) <|> importCmd.getTailPos?
-      return importId.raw.isMissing && keywordsTailPos.isSome && completionPos == keywordsTailPos.get! + ' '
-    | _ => unreachable!
+  return importsStx.any fun importStx => Id.run do
+    let importStx := importStx.raw
+    -- `importStx[0] == "private"?`
+    -- `importStx[1] == "meta"?`
+    let importCmd := importStx[2]
+    let allTk? := importStx[3].getOptional?
+    let importId := importStx[4]
+    let keywordsTailPos := allTk?.bind (·.getTailPos?) <|> importCmd.getTailPos?
+    return importId.isMissing && keywordsTailPos.isSome && completionPos == keywordsTailPos.get! + ' '
 
 /-- Checks whether `completionPos` points at a free space in the header. -/
 def isImportCmdCompletionRequest (headerStx : TSyntax ``Parser.Module.header) (completionPos : String.Pos) : Bool := Id.run do