feat: unknown identifier code action and the module system (#11164)

This PR ensures that the code action provided on unknown identifiers
correctly inserts `public` and/or `meta` in `module`s

src/Lean/Elab/Command.lean

@@ -377,7 +377,8 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArr
   let scope := s.scopes.head!
   let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
   let ctx := PartialContextInfo.commandCtx {
-    env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace,
+    env := s.env, cmdEnv? := some s.env, fileMap := ctx.fileMap, mctx := {},
+    currNamespace := scope.currNamespace,
     openDecls := scope.openDecls, options := scope.opts, ngen := s.ngen
   }
   return InfoTree.context ctx tree

src/Lean/Elab/InfoTree/Main.lean

@@ -52,7 +52,7 @@ def PartialContextInfo.mergeIntoOuter?
   | .autoImplicitCtx _, none =>
     panic! "Unexpected incomplete InfoTree context info."
   | .commandCtx innerInfo, some outer =>
-    some { outer with toCommandContextInfo := innerInfo }
+    some { outer with toCommandContextInfo := { innerInfo with cmdEnv? := outer.cmdEnv? <|> innerInfo.cmdEnv? } }
   | .parentDeclCtx innerParentDecl, some outer =>
     some { outer with parentDecl? := innerParentDecl }
   | .autoImplicitCtx innerAutoImplicits, some outer =>

src/Lean/Elab/InfoTree/Types.lean

@@ -18,12 +18,23 @@ public section
 namespace Lean.Elab
 
 /--
-Context after executing `liftTermElabM`.
+Context at the `CommandElabM/TermElabM` level. Created by `elabCommand` at the top level and then
+nestedly when relevant fields are affected (e.g. just before discarding the `mctx` when exiting from
+`TermElabM`).
+
 Note that the term information collected during elaboration may contain metavariables, and their
 assignments are stored at `mctx`.
 -/
 structure CommandContextInfo where
   env           : Environment
+  /--
+  Final environment at the end of `elabCommand`; empty for nested contexts. This environment can be
+  used to access information about the fully-elaborated current declaration such as declaration
+  ranges. It may not be a strict superset of `env` in case of backtracking, so `env` should be
+  preferred to access information about the elaboration context at the time this context object was
+  created.
+  -/
+  cmdEnv?       : Option Environment := none
   fileMap       : FileMap
   mctx          : MetavarContext := {}
   options       : Options        := {}

src/Lean/Elab/MutualDef.lean

@@ -1200,6 +1200,7 @@ where
       -- encoded name in e.g. kernel errors where it's hard to replace it)
       views.any (fun view => view.kind != .example || view.modifiers.isPublic) &&
       expandedDeclIds.any (!isPrivateName ·.declName)) do
+    withSaveInfoContext do  -- save adjusted env in info tree
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
@@ -1324,6 +1325,7 @@ where
     -- Never export private decls from theorem bodies to make sure they stay irrelevant for rebuilds
     withOptions (fun opts =>
       if headers.any (·.kind.isTheorem) then ResolveName.backward.privateInPublic.set opts false else opts) do
+    withSaveInfoContext do  -- save adjusted env in info tree
     let headers := headers.map fun header =>
       { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
     let values ← try

src/Lean/Server/CodeActions/UnknownIdentifier.lean

@@ -92,7 +92,7 @@ structure Insertion where
   edit     : TextEdit
 
 structure Query extends LeanModuleQuery where
-  env                : Environment
+  ctx                : Elab.ContextInfo
   determineInsertion : Name → Insertion
 
 partial def collectOpenNamespaces (currentNamespace : Name) (openDecls : List OpenDecl)
@@ -121,7 +121,7 @@ def computeIdQuery?
   return {
     identifier := id.toString
     openNamespaces := collectOpenNamespaces ctx.currNamespace ctx.openDecls
-    env := ctx.env
+    ctx
     determineInsertion decl :=
       let minimizedId := minimizeGlobalIdentifierInContext ctx.currNamespace ctx.openDecls decl
       {
@@ -155,7 +155,7 @@ def computeDotQuery?
   return some {
     identifier := String.Pos.Raw.extract text.source pos tailPos
     openNamespaces := typeNames.map (.allExcept · #[])
-    env := ctx.env
+    ctx
     determineInsertion decl :=
       {
         fullName := decl
@@ -186,7 +186,7 @@ def computeDotIdQuery?
   return some {
     identifier := id.toString
     openNamespaces := typeNames.map (.allExcept · #[])
-    env := ctx.env
+    ctx
     determineInsertion decl :=
       {
         fullName := decl
@@ -237,6 +237,22 @@ def importAllUnknownIdentifiersCodeAction (params : CodeActionParams) (kind : St
   }
 }
 
+private def mkImportText (ctx : Elab.ContextInfo) (mod : Name) :
+    String := Id.run do
+  let mut text := s!"import {mod}\n"
+  if let some parentDecl := ctx.parentDecl? then
+    if isMarkedMeta ctx.env parentDecl then
+      text := s!"meta {text}"
+      if !isPrivateName parentDecl then
+        -- As `meta` declarations go through a second, stricter visibility check in the compiler,
+        -- we should add `public` anywhere in a public definition (technically even private defs
+        -- could require public imports but that is not something we can check for here).
+        text := s!"public {text}"
+    else if ctx.env.isExporting then
+      -- Outside `meta`, add `public` only from public scope
+      text := s!"public {text}"
+  text
+
 def handleUnknownIdentifierCodeAction
     (id             : JsonRpc.RequestID)
     (params         : CodeActionParams)
@@ -276,8 +292,8 @@ def handleUnknownIdentifierCodeAction
     | return #[]
   for query in queries, result in response.queryResults do
     for ⟨mod, decl, isExactMatch⟩ in result do
-      let isDeclInEnv := query.env.contains decl
-      if ! isDeclInEnv && mod == query.env.mainModule then
+      let isDeclInEnv := query.ctx.env.contains decl
+      if ! isDeclInEnv && mod == query.ctx.env.mainModule then
         -- Don't offer any code actions for identifiers defined further down in the same file
         continue
       let insertion := query.determineInsertion decl
@@ -290,7 +306,7 @@ def handleUnknownIdentifierCodeAction
             edits := #[
               {
                 range := importInsertionRange
-                newText := s!"import {mod}\n"
+                newText := mkImportText query.ctx mod
               },
               insertion.edit
             ]
@@ -344,15 +360,15 @@ def handleResolveImportAllUnknownIdentifiersCodeAction?
   let mut imports : Std.HashSet Name := ∅
   for q in queries, result in response.queryResults do
     let some ⟨mod, decl, _⟩ := result.find? fun id =>
-        id.isExactMatch && ! q.env.contains id.decl
+        id.isExactMatch && ! q.ctx.env.contains id.decl
       | continue
-    if mod == q.env.mainModule then
+    if mod == q.ctx.env.mainModule then
       continue
     let insertion := q.determineInsertion decl
     if ! imports.contains mod then
       edits := edits.push {
         range := importInsertionRange
-        newText := s!"import {mod}\n"
+        newText := mkImportText q.ctx mod
       }
     edits := edits.push insertion.edit
     imports := imports.insert mod

src/Lean/Server/References.lean

@@ -86,19 +86,17 @@ def toLspRefInfo (i : RefInfo) : StateT Decls BaseIO Lsp.RefInfo := do
   let refToRefInfoLocation (ref : Reference) : StateT Decls BaseIO RefInfo.Location := do
     let parentDeclName? := ref.ci.parentDecl?
     let parentDeclNameString? := parentDeclName?.map (·.toString)
-    let .ok parentDeclInfo? ← EIO.toBaseIO <| ref.ci.runCoreM do
-        let some parentDeclName := parentDeclName?
-          | return none
-        -- Use `local` as it avoids unnecessary blocking, which is especially important when called
-        -- from the snapshot reporter. Specifically, if `ref` is from a tactic of an async theorem,
-        -- `parentDeclName` will not be available in the current environment and we would block only
-        -- to return `none` in the end anyway. At the end of elaboration, we rerun this function on
-        -- the full info tree with the main environment, so the access will succeed immediately.
-        let some parentDeclRanges := declRangeExt.find? (asyncMode := .local) (← getEnv) parentDeclName
-          | return none
-        return some <| .ofDeclarationRanges parentDeclRanges
-      -- we only use `CoreM` to get access to a `MonadEnv`, but these are currently all `IO`
-      | unreachable!
+    let parentDeclInfo? : Option DeclInfo := do
+      -- Use final command env that has decl ranges for current declaration as well
+      let cmdEnv ← ref.ci.cmdEnv?
+      let parentDeclName ← parentDeclName?
+      -- Use `local` as it avoids unnecessary blocking, which is especially important when called
+      -- from the snapshot reporter. Specifically, if `ref` is from a tactic of an async theorem,
+      -- `parentDeclName` will not be available in the current environment and we would block only
+      -- to return `none` in the end anyway. At the end of elaboration, we rerun this function on
+      -- the full info tree with the main environment, so the access will succeed immediately.
+      let parentDeclRanges ← declRangeExt.find? (asyncMode := .local) cmdEnv parentDeclName
+      return .ofDeclarationRanges parentDeclRanges
     if let some parentDeclNameString := parentDeclNameString? then
       if let some parentDeclInfo := parentDeclInfo? then
         modify (·.insert parentDeclNameString parentDeclInfo)

src/Lean/Server/Test/Runner.lean

@@ -692,9 +692,9 @@ partial def main (args : List String) : IO Unit := do
   let isProject := args[0]?.any (· == "-p")
   let (ipcCmd, ipcArgs) :=
     if isProject then
-      ("lake", #["serve", "--", "-DstderrAsMessages=false"])
+      ("lake", #["serve", "--", "-DstderrAsMessages=false", "-Dexperimental.module=true"])
     else
-      ("lean", #["--server", "-DstderrAsMessages=false"])
+      ("lean", #["--server", "-DstderrAsMessages=false", "-Dexperimental.module=true"])
   let path := if args.size == 1 then args[0]! else args[1]!
   let uri := s!"file:///{path}"
   -- We want `dbg_trace` tactics to write directly to stderr instead of being caught in reuse

tests/lean/interactive/unknownIdentifierCodeActions.lean

@@ -1,4 +1,8 @@
+module
 --^ waitForILeans
+
+public section
+
 #check Lean.Server.Test.Refs.test1
                                 --^ codeAction
 
@@ -48,3 +52,13 @@ example (f : Foobar) : Nat := f.veryLongAndHopefullyVeryUniqueBar
 
 example : Foobar := .veryLongAndHopefullyVeryUniqueFoobar
                                                        --^ codeAction
+
+def pubNonExposed : Lean.Server.Test.Refs.Test1
+                                             --^ codeAction
+  := Lean.Server.Test.Refs.Test1
+                              --^ codeAction
+
+public meta def pubMeta : Lean.Server.Test.Refs.Test1
+                                                   --^ codeAction
+  := Lean.Server.Test.Refs.Test1
+                              --^ codeAction

tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out

@@ -1,6 +1,6 @@
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 1, "character": 34}, "end": {"line": 1, "character": 34}},
+ {"start": {"line": 5, "character": 34}, "end": {"line": 5, "character": 34}},
  "context": {"diagnostics": []}}
 [{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -10,12 +10,12 @@
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 1, "character": 7},
-        "end": {"line": 1, "character": 34}},
+       {"start": {"line": 5, "character": 7},
+        "end": {"line": 5, "character": 34}},
        "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -25,16 +25,16 @@
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 1, "character": 7},
-        "end": {"line": 1, "character": 34}},
+       {"start": {"line": 5, "character": 7},
+        "end": {"line": 5, "character": 34}},
        "newText": "Lean.Server.Test.Refs.test10"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 4, "character": 33}, "end": {"line": 4, "character": 33}},
+ {"start": {"line": 8, "character": 33}, "end": {"line": 8, "character": 33}},
  "context": {"diagnostics": []}}
 [{"title": "Import LeanServerTestRefsTest0 from Lean.Server.Test.Refs",
   "kind": "refactor",
@@ -44,12 +44,12 @@
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 4, "character": 10},
-        "end": {"line": 4, "character": 33}},
+       {"start": {"line": 8, "character": 10},
+        "end": {"line": 8, "character": 33}},
        "newText": "LeanServerTestRefsTest0"}]}]}},
  {"title":
   "Import Lean.Server.Test.LeanServerTestRefsTest0' from Lean.Server.Test.Refs",
@@ -60,12 +60,12 @@
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 4, "character": 10},
-        "end": {"line": 4, "character": 33}},
+       {"start": {"line": 8, "character": 10},
+        "end": {"line": 8, "character": 33}},
        "newText": "Lean.Server.Test.LeanServerTestRefsTest0'"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
   "kind": "refactor",
@@ -75,12 +75,12 @@
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 4, "character": 10},
-        "end": {"line": 4, "character": 33}},
+       {"start": {"line": 8, "character": 10},
+        "end": {"line": 8, "character": 33}},
        "newText": "Lean.Server.Test.Refs.test10"}]}]}},
  {"title": "Import all unambiguous unknown identifiers",
   "kind": "quickfix",
@@ -90,8 +90,8 @@
    "params":
    {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
     "range":
-    {"start": {"line": 4, "character": 33},
-     "end": {"line": 4, "character": 33}},
+    {"start": {"line": 8, "character": 33},
+     "end": {"line": 8, "character": 33}},
     "context": {"diagnostics": []}}}}]
 Resolution of Import all unambiguous unknown identifiers:
 {"title": "Import all unambiguous unknown identifiers",
@@ -102,20 +102,36 @@ Resolution of Import all unambiguous unknown identifiers:
     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
     "edits":
     [{"range":
-      {"start": {"line": 0, "character": 0},
-       "end": {"line": 0, "character": 0}},
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
       "newText": "import Lean.Server.Test.Refs\n"},
      {"range":
-      {"start": {"line": 13, "character": 7},
-       "end": {"line": 13, "character": 48}},
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
       "newText": "LeanServerTestRefsTest0'"},
      {"range":
-      {"start": {"line": 24, "character": 7},
-       "end": {"line": 24, "character": 34}},
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
       "newText": "Test1"},
      {"range":
-      {"start": {"line": 4, "character": 10},
-       "end": {"line": 4, "character": 33}},
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
       "newText": "LeanServerTestRefsTest0"}]}]},
  "data":
  {"providerResultIndex": 0,
@@ -123,11 +139,11 @@ Resolution of Import all unambiguous unknown identifiers:
   "params":
   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
    "range":
-   {"start": {"line": 4, "character": 33}, "end": {"line": 4, "character": 33}},
+   {"start": {"line": 8, "character": 33}, "end": {"line": 8, "character": 33}},
    "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 8, "character": 34}, "end": {"line": 8, "character": 34}},
+ {"start": {"line": 12, "character": 34}, "end": {"line": 12, "character": 34}},
  "context": {"diagnostics": []}}
 [{"title": "Import Test1 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -137,12 +153,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 8, "character": 7},
-        "end": {"line": 8, "character": 34}},
+       {"start": {"line": 12, "character": 7},
+        "end": {"line": 12, "character": 34}},
        "newText": "Test1"}]}]}},
  {"title": "Import test10 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -152,16 +168,16 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 8, "character": 7},
-        "end": {"line": 8, "character": 34}},
+       {"start": {"line": 12, "character": 7},
+        "end": {"line": 12, "character": 34}},
        "newText": "test10"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 17, "character": 34}, "end": {"line": 17, "character": 34}},
+ {"start": {"line": 21, "character": 34}, "end": {"line": 21, "character": 34}},
  "context": {"diagnostics": []}}
 [{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -171,12 +187,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 17, "character": 7},
-        "end": {"line": 17, "character": 34}},
+       {"start": {"line": 21, "character": 7},
+        "end": {"line": 21, "character": 34}},
        "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -186,16 +202,16 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 17, "character": 7},
-        "end": {"line": 17, "character": 34}},
+       {"start": {"line": 21, "character": 7},
+        "end": {"line": 21, "character": 34}},
        "newText": "Lean.Server.Test.Refs.test10"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 20, "character": 33}, "end": {"line": 20, "character": 33}},
+ {"start": {"line": 24, "character": 33}, "end": {"line": 24, "character": 33}},
  "context": {"diagnostics": []}}
 [{"title": "Import Lean.Server.Test.Refs.test9 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -205,12 +221,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.test9"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test8 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -220,12 +236,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.test8"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test7 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -235,12 +251,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.test7"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test6 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -250,12 +266,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test6"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test5 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -265,12 +281,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test5"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test4 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -280,12 +296,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test4"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test3 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -295,12 +311,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test3"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test2 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -310,12 +326,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test2"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -325,12 +341,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
  {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -340,16 +356,16 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 20, "character": 7},
-        "end": {"line": 20, "character": 33}},
+       {"start": {"line": 24, "character": 7},
+        "end": {"line": 24, "character": 33}},
        "newText": "Lean.Server.Test.Refs.test10"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 24, "character": 34}, "end": {"line": 24, "character": 34}},
+ {"start": {"line": 28, "character": 34}, "end": {"line": 28, "character": 34}},
  "context": {"diagnostics": []}}
 [{"title": "Import Test1 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -359,12 +375,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 24, "character": 7},
-        "end": {"line": 24, "character": 34}},
+       {"start": {"line": 28, "character": 7},
+        "end": {"line": 28, "character": 34}},
        "newText": "Test1"}]}]}},
  {"title": "Import test10 from Lean.Server.Test.Refs",
   "kind": "quickfix",
@@ -374,12 +390,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 0, "character": 0},
-        "end": {"line": 0, "character": 0}},
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
        "newText": "import Lean.Server.Test.Refs\n"},
       {"range":
-       {"start": {"line": 24, "character": 7},
-        "end": {"line": 24, "character": 34}},
+       {"start": {"line": 28, "character": 7},
+        "end": {"line": 28, "character": 34}},
        "newText": "test10"}]}]}},
  {"title": "Import all unambiguous unknown identifiers",
   "kind": "quickfix",
@@ -389,8 +405,8 @@ Resolution of Import all unambiguous unknown identifiers:
    "params":
    {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
     "range":
-    {"start": {"line": 24, "character": 34},
-     "end": {"line": 24, "character": 34}},
+    {"start": {"line": 28, "character": 34},
+     "end": {"line": 28, "character": 34}},
     "context": {"diagnostics": []}}}}]
 Resolution of Import all unambiguous unknown identifiers:
 {"title": "Import all unambiguous unknown identifiers",
@@ -401,20 +417,36 @@ Resolution of Import all unambiguous unknown identifiers:
     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
     "edits":
     [{"range":
-      {"start": {"line": 0, "character": 0},
-       "end": {"line": 0, "character": 0}},
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
       "newText": "import Lean.Server.Test.Refs\n"},
      {"range":
-      {"start": {"line": 13, "character": 7},
-       "end": {"line": 13, "character": 48}},
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
       "newText": "LeanServerTestRefsTest0'"},
      {"range":
-      {"start": {"line": 24, "character": 7},
-       "end": {"line": 24, "character": 34}},
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
       "newText": "Test1"},
      {"range":
-      {"start": {"line": 4, "character": 10},
-       "end": {"line": 4, "character": 33}},
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
       "newText": "LeanServerTestRefsTest0"}]}]},
  "data":
  {"providerResultIndex": 0,
@@ -422,12 +454,12 @@ Resolution of Import all unambiguous unknown identifiers:
   "params":
   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
    "range":
-   {"start": {"line": 24, "character": 34},
-    "end": {"line": 24, "character": 34}},
+   {"start": {"line": 28, "character": 34},
+    "end": {"line": 28, "character": 34}},
    "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 42, "character": 40}, "end": {"line": 42, "character": 40}},
+ {"start": {"line": 46, "character": 40}, "end": {"line": 46, "character": 40}},
  "context": {"diagnostics": []}}
 [{"title": "Change to veryLongAndHopefullyVeryUniqueFoo0",
   "kind": "quickfix",
@@ -437,8 +469,8 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 42, "character": 7},
-        "end": {"line": 42, "character": 40}},
+       {"start": {"line": 46, "character": 7},
+        "end": {"line": 46, "character": 40}},
        "newText": "veryLongAndHopefullyVeryUniqueFoo0"}]}]}},
  {"title": "Change to veryLongAndHopefullyVeryUniqueFoobar0",
   "kind": "quickfix",
@@ -448,12 +480,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 42, "character": 7},
-        "end": {"line": 42, "character": 40}},
+       {"start": {"line": 46, "character": 7},
+        "end": {"line": 46, "character": 40}},
        "newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 45, "character": 65}, "end": {"line": 45, "character": 65}},
+ {"start": {"line": 49, "character": 65}, "end": {"line": 49, "character": 65}},
  "context": {"diagnostics": []}}
 [{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueBar0",
   "kind": "quickfix",
@@ -463,12 +495,12 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 45, "character": 32},
-        "end": {"line": 45, "character": 65}},
+       {"start": {"line": 49, "character": 32},
+        "end": {"line": 49, "character": 65}},
        "newText": "veryLongAndHopefullyVeryUniqueBar0"}]}]}}]
 {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
  "range":
- {"start": {"line": 48, "character": 57}, "end": {"line": 48, "character": 57}},
+ {"start": {"line": 52, "character": 57}, "end": {"line": 52, "character": 57}},
  "context": {"diagnostics": []}}
 [{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueFoobar0",
   "kind": "quickfix",
@@ -478,6 +510,382 @@ Resolution of Import all unambiguous unknown identifiers:
      {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
      "edits":
      [{"range":
-       {"start": {"line": 48, "character": 21},
-        "end": {"line": 48, "character": 57}},
+       {"start": {"line": 52, "character": 21},
+        "end": {"line": 52, "character": 57}},
        "newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}]
+{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+ "range":
+ {"start": {"line": 55, "character": 47}, "end": {"line": 55, "character": 47}},
+ "context": {"diagnostics": []}}
+[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 55, "character": 20},
+        "end": {"line": 55, "character": 47}},
+       "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
+ {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 55, "character": 20},
+        "end": {"line": 55, "character": 47}},
+       "newText": "Lean.Server.Test.Refs.test10"}]}]}},
+ {"title": "Import all unambiguous unknown identifiers",
+  "kind": "quickfix",
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "unknownIdentifiers",
+   "params":
+   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+    "range":
+    {"start": {"line": 55, "character": 47},
+     "end": {"line": 55, "character": 47}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Import all unambiguous unknown identifiers:
+{"title": "Import all unambiguous unknown identifiers",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
+      "newText": "import Lean.Server.Test.Refs\n"},
+     {"range":
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
+      "newText": "LeanServerTestRefsTest0'"},
+     {"range":
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
+      "newText": "Test1"},
+     {"range":
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
+      "newText": "LeanServerTestRefsTest0"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "unknownIdentifiers",
+  "params":
+  {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+   "range":
+   {"start": {"line": 55, "character": 47},
+    "end": {"line": 55, "character": 47}},
+   "context": {"diagnostics": []}}}}
+{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+ "range":
+ {"start": {"line": 57, "character": 32}, "end": {"line": 57, "character": 32}},
+ "context": {"diagnostics": []}}
+[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 57, "character": 5},
+        "end": {"line": 57, "character": 32}},
+       "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
+ {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 57, "character": 5},
+        "end": {"line": 57, "character": 32}},
+       "newText": "Lean.Server.Test.Refs.test10"}]}]}},
+ {"title": "Import all unambiguous unknown identifiers",
+  "kind": "quickfix",
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "unknownIdentifiers",
+   "params":
+   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+    "range":
+    {"start": {"line": 57, "character": 32},
+     "end": {"line": 57, "character": 32}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Import all unambiguous unknown identifiers:
+{"title": "Import all unambiguous unknown identifiers",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
+      "newText": "import Lean.Server.Test.Refs\n"},
+     {"range":
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
+      "newText": "LeanServerTestRefsTest0'"},
+     {"range":
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
+      "newText": "Test1"},
+     {"range":
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
+      "newText": "LeanServerTestRefsTest0"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "unknownIdentifiers",
+  "params":
+  {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+   "range":
+   {"start": {"line": 57, "character": 32},
+    "end": {"line": 57, "character": 32}},
+   "context": {"diagnostics": []}}}}
+{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+ "range":
+ {"start": {"line": 60, "character": 53}, "end": {"line": 60, "character": 53}},
+ "context": {"diagnostics": []}}
+[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public meta import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 60, "character": 26},
+        "end": {"line": 60, "character": 53}},
+       "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
+ {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public meta import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 60, "character": 26},
+        "end": {"line": 60, "character": 53}},
+       "newText": "Lean.Server.Test.Refs.test10"}]}]}},
+ {"title": "Import all unambiguous unknown identifiers",
+  "kind": "quickfix",
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "unknownIdentifiers",
+   "params":
+   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+    "range":
+    {"start": {"line": 60, "character": 53},
+     "end": {"line": 60, "character": 53}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Import all unambiguous unknown identifiers:
+{"title": "Import all unambiguous unknown identifiers",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
+      "newText": "import Lean.Server.Test.Refs\n"},
+     {"range":
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
+      "newText": "LeanServerTestRefsTest0'"},
+     {"range":
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
+      "newText": "Test1"},
+     {"range":
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
+      "newText": "LeanServerTestRefsTest0"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "unknownIdentifiers",
+  "params":
+  {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+   "range":
+   {"start": {"line": 60, "character": 53},
+    "end": {"line": 60, "character": 53}},
+   "context": {"diagnostics": []}}}}
+{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+ "range":
+ {"start": {"line": 62, "character": 32}, "end": {"line": 62, "character": 32}},
+ "context": {"diagnostics": []}}
+[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public meta import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 62, "character": 5},
+        "end": {"line": 62, "character": 32}},
+       "newText": "Lean.Server.Test.Refs.Test1"}]}]}},
+ {"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
+  "kind": "quickfix",
+  "edit":
+  {"documentChanges":
+   [{"textDocument":
+     {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+     "edits":
+     [{"range":
+       {"start": {"line": 1, "character": 0},
+        "end": {"line": 1, "character": 0}},
+       "newText": "public meta import Lean.Server.Test.Refs\n"},
+      {"range":
+       {"start": {"line": 62, "character": 5},
+        "end": {"line": 62, "character": 32}},
+       "newText": "Lean.Server.Test.Refs.test10"}]}]}},
+ {"title": "Import all unambiguous unknown identifiers",
+  "kind": "quickfix",
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "unknownIdentifiers",
+   "params":
+   {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+    "range":
+    {"start": {"line": 62, "character": 32},
+     "end": {"line": 62, "character": 32}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Import all unambiguous unknown identifiers:
+{"title": "Import all unambiguous unknown identifiers",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 1, "character": 0},
+       "end": {"line": 1, "character": 0}},
+      "newText": "import Lean.Server.Test.Refs\n"},
+     {"range":
+      {"start": {"line": 17, "character": 7},
+       "end": {"line": 17, "character": 48}},
+      "newText": "LeanServerTestRefsTest0'"},
+     {"range":
+      {"start": {"line": 28, "character": 7},
+       "end": {"line": 28, "character": 34}},
+      "newText": "Test1"},
+     {"range":
+      {"start": {"line": 55, "character": 20},
+       "end": {"line": 55, "character": 47}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 57, "character": 5},
+       "end": {"line": 57, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 60, "character": 26},
+       "end": {"line": 60, "character": 53}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 62, "character": 5},
+       "end": {"line": 62, "character": 32}},
+      "newText": "Lean.Server.Test.Refs.Test1"},
+     {"range":
+      {"start": {"line": 8, "character": 10},
+       "end": {"line": 8, "character": 33}},
+      "newText": "LeanServerTestRefsTest0"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "unknownIdentifiers",
+  "params":
+  {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
+   "range":
+   {"start": {"line": 62, "character": 32},
+    "end": {"line": 62, "character": 32}},
+   "context": {"diagnostics": []}}}}