Documentation

Lean.Data.Lsp.Internal

inductive Lean.Lsp.RefIdent :

Type

const: Lean.Name → Lean.Lsp.RefIdent
fvar: Lean.FVarId → Lean.Lsp.RefIdent

instance Lean.Lsp.instBEqRefIdent :

BEq Lean.Lsp.RefIdent

Equations

Lean.Lsp.instBEqRefIdent = { beq := [anonymous] }

instance Lean.Lsp.instInhabitedRefIdent :

Inhabited Lean.Lsp.RefIdent

Equations

Lean.Lsp.instInhabitedRefIdent = { default := Lean.Lsp.RefIdent.const default }

instance Lean.Lsp.instHashableRefIdent :

Hashable Lean.Lsp.RefIdent

Equations

Lean.Lsp.instHashableRefIdent = { hash := [anonymous] }

def Lean.Lsp.RefIdent.toString :

Lean.Lsp.RefIdent → String

Equations

Lean.Lsp.RefIdent.toString x = match x with | Lean.Lsp.RefIdent.const n => toString "c:" ++ toString n ++ toString "" | Lean.Lsp.RefIdent.fvar id => toString "f:" ++ toString id.name ++ toString ""

def Lean.Lsp.RefIdent.fromString (s : String) :

Except String Lean.Lsp.RefIdent

Equations

Lean.Lsp.RefIdent.fromString s = let sPrefix := String.take s 2; let sName := String.drop s 2; let _do_jp := fun name => match sPrefix with | "c:" => pure (Lean.Lsp.RefIdent.const name) | "f:" => pure (Lean.Lsp.RefIdent.fvar { name := name }) | x => throw "string must start with 'c:' or 'f:'"; match sName with | "[anonymous]" => do let y ← pure Lean.Name.anonymous _do_jp y | x => match Lean.Syntax.decodeNameLit ("`" ++ sName) with | some n => do let y ← pure n _do_jp y | none => do let y ← throw (toString "expected a Name, got " ++ toString sName ++ toString "") _do_jp y

structure Lean.Lsp.RefInfo :

Type

definition : Option Lean.Lsp.Range
usages : Array Lean.Lsp.Range

instance Lean.Lsp.instToJsonRefInfo :

Lean.ToJson Lean.Lsp.RefInfo

Equations

Lean.Lsp.instToJsonRefInfo = { toJson := fun i => let rangeToList := fun r => [r.start.line, r.start.character, r.end.line, r.end.character]; Lean.Json.mkObj [("definition", Lean.toJson (Option.map rangeToList i.definition)), ("usages", Lean.toJson (Array.map rangeToList i.usages))] }

instance Lean.Lsp.instFromJsonRefInfo :

Lean.FromJson Lean.Lsp.RefInfo

Equations

Lean.Lsp.instFromJsonRefInfo = { fromJson? := fun j => let listToRange := fun l => match l with | [sLine, sChar, eLine, eChar] => pure { start := { line := sLine, character := sChar }, end := { line := eLine, character := eChar } } | x => throw (toString "Expected list of length 4, not " ++ toString (List.length l) ++ toString ""); do let definition ← Lean.Json.getObjValAs? j (Option (List Nat)) "definition" let _do_jp : Option Lean.Lsp.Range → Except String Lean.Lsp.RefInfo := fun definition => do let usages ← Lean.Json.getObjValAs? j (Array (List Nat)) "usages" let usages ← Array.mapM listToRange usages pure { definition := definition, usages := usages } match definition with | none => do let y ← pure none _do_jp y | some list => do let y ← some <$> listToRange list _do_jp y }

noncomputable def Lean.Lsp.ModuleRefs :

Type

Equations

Lean.Lsp.ModuleRefs = Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo

instance Lean.Lsp.instToJsonModuleRefs :

Lean.ToJson Lean.Lsp.ModuleRefs

Equations

Lean.Lsp.instToJsonModuleRefs = { toJson := fun m => Lean.Json.mkObj (List.map (fun x => match x with | (ident, info) => (Lean.Lsp.RefIdent.toString ident, Lean.toJson info)) (Std.HashMap.toList m)) }

instance Lean.Lsp.instFromJsonModuleRefs :

Lean.FromJson Lean.Lsp.ModuleRefs

Equations

Lean.Lsp.instFromJsonModuleRefs = { fromJson? := fun j => do let node ← Lean.Json.getObj? j Std.RBNode.foldM (fun m k v => do let a ← Lean.Lsp.RefIdent.fromString k let a_1 ← Lean.fromJson? v pure (Std.HashMap.insert m a a_1)) Std.HashMap.empty node }

structure Lean.Lsp.LeanIleanInfoParams :

Type

version : Nat
references : Lean.Lsp.ModuleRefs

instance Lean.Lsp.instFromJsonLeanIleanInfoParams :

Lean.FromJson Lean.Lsp.LeanIleanInfoParams

Equations

Lean.Lsp.instFromJsonLeanIleanInfoParams = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonLeanIleanInfoParams :

Lean.ToJson Lean.Lsp.LeanIleanInfoParams

Equations

Lean.Lsp.instToJsonLeanIleanInfoParams = { toJson := [anonymous] }