feat: add addional CompletionInfo

src/Lean/Elab/App.lean

@@ -774,7 +774,7 @@ false, no elaboration function executed by `x` will reset it to
 private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr))
     : TermElabM (Array (TermElabResult Expr)) := do
-  let funLVals ← withRef fIdent <| resolveName' fIdent fExplicitUnivs
+  let funLVals ← withRef fIdent <| resolveName' fIdent fExplicitUnivs expectedType?
   let overloaded := overloaded || funLVals.length > 1
   -- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do

src/Lean/Elab/Command.lean

@@ -415,8 +415,13 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
     popScopes n
     throwError "invalid 'end', insufficient scopes"
   match header? with
-  | none        => unless checkAnonymousScope scopes do throwError "invalid 'end', name is missing"
-  | some header => unless checkEndHeader header scopes do throwError "invalid 'end', name mismatch"
+  | none        =>
+    unless checkAnonymousScope scopes do
+      throwError "invalid 'end', name is missing"
+  | some header =>
+    unless checkEndHeader header scopes do
+      addCompletionInfo <| CompletionInfo.endSection stx (scopes.map fun scope => scope.header)
+      throwError "invalid 'end', name mismatch"
 
 @[inline] def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
   addNamespace ns

src/Lean/Elab/InfoTree.lean

@@ -40,15 +40,19 @@ structure CommandInfo where
 inductive CompletionInfo where
   | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
   | id (stx : Syntax) (expectedType? : Option Expr)
+  | namespaceId (stx : Syntax)
   | option (stx : Syntax)
-  | endSection (stx : Syntax)
+  | endSection (stx : Syntax) (scopeNames : List String)
+  | tactic (stx : Syntax) (goals : List MVarId)
   -- TODO `import`
 
 def CompletionInfo.stx : CompletionInfo → Syntax
   | dot i .. => i.stx
   | id stx .. => stx
+  | namespaceId stx => stx
   | option stx => stx
-  | endSection stx => stx
+  | endSection stx .. => stx
+  | tactic stx .. => stx
 
 structure FieldInfo where
   name : Name
@@ -112,7 +116,7 @@ class MonadInfoTree (m : Type → Type)  where
 
 export MonadInfoTree (getInfoState modifyInfoState)
 
-instance (m n) [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
+instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
   getInfoState      := liftM (getInfoState : m _)
   modifyInfoState f := liftM (modifyInfoState f : m _)
 
@@ -224,6 +228,9 @@ def pushInfoLeaf (t : Info) : m Unit := do
   if (← getInfoState).enabled then
     pushInfoTree <| InfoTree.node (children := {}) t
 
+def addCompletionInfo (info : CompletionInfo) : m Unit := do
+  pushInfoLeaf <| Info.ofCompletionInfo info
+
 def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) : m Name := do
   let n ← resolveGlobalConstNoOverload id
   if (← getInfoState).enabled then

src/Lean/Elab/SetOption.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Log
-
+import Lean.Elab.InfoTree
 namespace Lean.Elab
 
 variable [Monad m] [MonadOptions m] [MonadExceptOf Exception m] [MonadRef m]
-variable [AddErrorMessageContext m] [MonadLiftT (EIO Exception) m]
+variable [AddErrorMessageContext m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m]
 
 def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let optionName := id.getId.eraseMacroScopes
@@ -24,7 +24,12 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   | _ => throwError "unexpected set_option value {val}"
 where
   setOption (optionName : Name) (val : DataValue) : m Options := do
-    let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName)
+    let decl ←
+      try
+        IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName)
+      catch ex =>
+        addCompletionInfo <| CompletionInfo.option id
+        throw ex
     unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
     return (← getOptions).insert optionName val
 

src/Lean/Elab/Tactic/Basic.lean

@@ -435,7 +435,8 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtinTactic skip] def evalSkip : Tactic := fun stx => pure ()
 
-@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => pure ()
+@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do
+  addCompletionInfo <| CompletionInfo.tactic stx (← getGoals)
 
 @[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do
   let tactic := stx[1]

src/Lean/Elab/Term.lean

@@ -1076,7 +1076,7 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
 
 /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/
 def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do
-  pushInfoLeaf <| Info.ofCompletionInfo <| CompletionInfo.dot { expr := e, stx := stx, lctx := (← getLCtx) } (field? := field?) (expectedType? := expectedType?)
+  addCompletionInfo <| CompletionInfo.dot { expr := e, stx := stx, lctx := (← getLCtx) } (field? := field?) (expectedType? := expectedType?)
 
 /--
   Main function for elaborating terms.
@@ -1335,18 +1335,23 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
    let const ← mkConst constName explicitLevels
    return (const, projs) :: result
 
-def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
-  if let some (e, projs) ← resolveLocalName n then
-    unless explicitLevels.isEmpty do
-      throwError "invalid use of explicit universe parameters, '{e}' is a local"
-    return [(e, projs)]
-  -- check for section variable capture by a quotation
-  if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then
-    return [(e, projs)]  -- section variables should shadow global decls
-  if preresolved.isEmpty then
-    process (← resolveGlobalName n)
-  else
-    process preresolved
+def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none): TermElabM (List (Expr × List String)) := do
+  try
+    if let some (e, projs) ← resolveLocalName n then
+      unless explicitLevels.isEmpty do
+        throwError "invalid use of explicit universe parameters, '{e}' is a local"
+      return [(e, projs)]
+    -- check for section variable capture by a quotation
+    if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then
+      return [(e, projs)]  -- section variables should shadow global decls
+    if preresolved.isEmpty then
+      process (← resolveGlobalName n)
+    else
+      process preresolved
+  catch ex =>
+    if preresolved.isEmpty && explicitLevels.isEmpty then
+      addCompletionInfo <| CompletionInfo.id stx expectedType?
+    throw ex
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then
     if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n then
@@ -1359,10 +1364,10 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
   `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   match ident with
   | Syntax.ident info rawStr n preresolved =>
-    let r ← resolveName n preresolved explicitLevels
+    let r ← resolveName ident n preresolved explicitLevels expectedType?
     r.mapM fun (c, fields) => do
       let (cSstr, fields) := fields.foldr (init := (rawStr, [])) fun field (restSstr, fs) =>
         let fieldSstr := restSstr.takeRightWhile (· ≠ '.')
@@ -1392,7 +1397,7 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) : TermElabM (Lis
 def resolveId? (stx : Syntax) (kind := "term") : TermElabM (Option Expr) :=
   match stx with
   | Syntax.ident _ _ val preresolved => do
-    let rs ← try resolveName val preresolved [] catch _ => pure []
+    let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨f, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with