fix: implement suggestions

src/Lean/Data/Lsp/Basic.lean

@@ -31,16 +31,11 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally.
 structure Position where
   line : Nat
   character : Nat
-  deriving Inhabited, BEq, Hashable, ToJson, FromJson
+  deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson
 
 instance : ToString Position := ⟨fun p =>
   "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
 
-instance : Ord Position where
-  compare a b := match compare a.line b.line with
-    | Ordering.eq => compare a.character b.character
-    | o => o
-
 instance : LT Position := ltOfOrd
 instance : LE Position := leOfOrd
 

src/Lean/Data/Lsp/Internal.lean

@@ -32,17 +32,16 @@ def toString : RefIdent → String
 def fromString (s : String) : Except String RefIdent := do
   let sPrefix := s.take 2
   let sName := s.drop 2
-  let mk ← match sPrefix with
-    | "c:" => RefIdent.const
-    | "f:" => fun n => RefIdent.fvar <| FVarId.mk n
-    | _ => throw "string must start with 'c:' or 'f:'"
   -- See `FromJson Name`
   let name ← match sName with
     | "[anonymous]" => Name.anonymous
     | _ => match Syntax.decodeNameLit ("`" ++ sName) with
       | some n => n
       | none => throw s!"expected a Name, got {sName}"
-  mk name
+  match sPrefix with
+    | "c:" => RefIdent.const name
+    | "f:" => RefIdent.fvar <| FVarId.mk name
+    | _ => throw "string must start with 'c:' or 'f:'"
 
 end RefIdent
 

src/Lean/Elab/Frontend.lean

@@ -101,7 +101,7 @@ def runFrontend
     (fileName : String)
     (mainModuleName : Name)
     (trustLevel : UInt32 := 0)
-    (ileanFileName: Option String := none)
+    (ileanFileName? : Option String := none)
     : IO (Environment × Bool) := do
   let inputCtx := Parser.mkInputContext input fileName
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
@@ -109,16 +109,16 @@ def runFrontend
   let env := env.setMainModule mainModuleName
   let mut commandState := Command.mkState env messages opts
 
-  if ileanFileName.isSome then
+  if ileanFileName?.isSome then
     -- Collect InfoTrees so we can later extract and export their info to the ilean file
-    commandState := { commandState with infoState := { commandState.infoState with enabled := true }}
+    commandState := { commandState with infoState.enabled := true }
 
   let s ← IO.processCommands inputCtx parserState commandState
   for msg in s.commandState.messages.toList do
     IO.print (← msg.toString (includeEndPos := getPrintMessageEndPos opts))
 
-  if let some ileanFileName := ileanFileName then
-    let trees := s.commandState.infoState.trees.toList
+  if let some ileanFileName := ileanFileName? then
+    let trees := s.commandState.infoState.trees.toArray
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ toString $ toJson ilean

src/Lean/Server/FileWorker.lean

@@ -70,9 +70,7 @@ section Elab
     snaps : List Snapshot
 
   private def AsyncElabState.lastSnap (s : AsyncElabState) : Snapshot :=
-    match s.snaps.getLast? with
-      | some snap => snap
-      | none => s.headerSnap
+    s.snaps.getLastD s.headerSnap
 
   abbrev AsyncElabM := StateT AsyncElabState $ ExceptT ElabTaskError IO
 

src/Lean/Server/References.lean

@@ -46,9 +46,9 @@ def contains (self : RefInfo) (pos : Lsp.Position) : Bool := Id.run do
     if contains range pos then
       return true
   false
-  where
-    contains (range : Lsp.Range) (pos : Lsp.Position) : Bool :=
-      range.start <= pos && pos < range.end
+where
+  contains (range : Lsp.Range) (pos : Lsp.Position) : Bool :=
+    range.start <= pos && pos < range.end
 
 end Lean.Lsp.RefInfo
 
@@ -141,10 +141,10 @@ def combineFvars (refs : Array Reference) : Array Reference := Id.run do
     | { ident := ident@(RefIdent.fvar _), range, isDeclaration := false } =>
       refs.push { ident := applyIdMap idMap ident, range, isDeclaration := false }
     | _ => refs.push ref
-  where
-    applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent
-      | m, RefIdent.fvar id => RefIdent.fvar <| m.findD id id
-      | _, ident => ident
+where
+  applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent
+    | m, RefIdent.fvar id => RefIdent.fvar <| m.findD id id
+    | _, ident => ident
 
 def findModuleRefs (text : FileMap) (trees : List InfoTree) (localVars : Bool := true)
     : ModuleRefs := Id.run do
@@ -194,7 +194,7 @@ def findAt? (self : References) (module : Name) (pos : Lsp.Position) : Option Re
     return refs.findAt? pos
   none
 
-def referingTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
+def referringTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
     (includeDefinition : Bool := true) : IO (Array Location) := do
   let mut result := #[]
   for (module, refs) in self.allRefs.toList do

src/Lean/Server/Watchdog.lean

@@ -359,7 +359,7 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
     if let some module ← searchModuleNameOfFileName path srcSearchPath then
       let references ← (← read).references.get
       if let some ident := references.findAt? module p.position then
-        return ← references.referingTo ident srcSearchPath p.context.includeDeclaration
+        return ← references.referringTo ident srcSearchPath p.context.includeDeclaration
   #[]
 
 end RequestHandling