Equations
- Lean.Server.FileWorker.handleCompletion p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let pos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.toTextDocumentPositionParams.position let a ← read let caps : Lean.Lsp.ClientCapabilities := a.initParams.capabilities Lean.Server.RequestM.withWaitFindSnap doc (fun a => decide (Lean.Server.Snapshots.Snapshot.endPos a + 1 ≥ pos)) (pure { isIncomplete := true, items := #[] }) fun snap => do let a ← liftM (Lean.Server.Completion.find? doc.meta.text pos (Lean.Server.Snapshots.Snapshot.infoTree snap) caps) let _do_jp : PUnit → Lean.Server.RequestM Lean.Lsp.CompletionList := fun y => pure { isIncomplete := true, items := #[] } match a with | some r => pure r | x => do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Server.FileWorker.handleHover p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let mkHover : String → String.Pos → String.Pos → Lean.Lsp.Hover := fun s f t => { contents := { kind := Lean.Lsp.MarkupKind.markdown, value := s }, range? := some { start := Lean.FileMap.utf8PosToLspPos text f, end := Lean.FileMap.utf8PosToLspPos text t } } let hoverPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.toTextDocumentPositionParams.position Lean.Server.RequestM.withWaitFindSnap doc (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s > hoverPos)) (pure none) fun snap => let _do_jp := fun y => pure none; match Lean.Elab.InfoTree.hoverableInfoAt? (Lean.Server.Snapshots.Snapshot.infoTree snap) hoverPos with | some (ci, i) => do let a ← liftM (Lean.Elab.Info.fmtHover? ci i) match a with | some hoverFmt => pure (some (mkHover (toString hoverFmt) (Option.get! (Lean.Elab.Info.pos? i)) (Option.get! (Lean.Elab.Info.tailPos? i)))) | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y
- declaration: Lean.Server.FileWorker.GoToKind
- definition: Lean.Server.FileWorker.GoToKind
- type: Lean.Server.FileWorker.GoToKind
Equations
- Lean.Server.FileWorker.instBEqGoToKind = { beq := [anonymous] }
def
Lean.Server.FileWorker.handleDefinition
(kind : Lean.Server.FileWorker.GoToKind)
(p : Lean.Lsp.TextDocumentPositionParams)
:
Equations
- Lean.Server.FileWorker.handleDefinition kind p = do let rc ← read let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let hoverPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.position let documentUriFromModule : Lean.Name → Lean.MetaM (Option Lean.Lsp.DocumentUri) := fun modName => do let discr ← liftM (Lean.SearchPath.findWithExt rc.srcSearchPath "lean" modName) match discr with | some modFname => do let modFname ← liftM (IO.FS.realPath modFname) pure (some (Lean.Lsp.DocumentUri.ofPath modFname)) | x => pure none let locationLinksFromDecl : Lean.Elab.Info → Lean.Name → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun i n => do let mod? ← Lean.findModuleOf? n let _do_jp : Option Lean.Lsp.DocumentUri → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun modUri? => do let ranges? ← Lean.findDeclarationRanges? n let _do_jp : PUnit → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun y => pure #[] match (ranges?, modUri?) with | (some ranges, some modUri) => let declRangeToLspRange := fun r => { start := { line := r.pos.line - 1, character := r.charUtf16 }, end := { line := r.endPos.line - 1, character := r.endCharUtf16 } }; let ll := { originSelectionRange? := (fun a => String.Range.toLspRange text a) <$> Lean.Elab.Info.range? i, targetUri := modUri, targetRange := declRangeToLspRange ranges.range, targetSelectionRange := declRangeToLspRange ranges.selectionRange }; pure #[ll] | x => do let y ← pure PUnit.unit _do_jp y match mod? with | some modName => do let y ← documentUriFromModule modName _do_jp y | none => do let y ← pure (some doc.meta.uri) _do_jp y let locationLinksFromBinder : Lean.Elab.InfoTree → Lean.Elab.Info → Lean.FVarId → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun t i id => let _do_jp := fun y => pure #[]; match Lean.Elab.InfoTree.findInfo? (fun x => match x with | Lean.Elab.Info.ofTermInfo { toElabInfo := { elaborator := x_1, stx := x_2 }, lctx := x_3, expectedType? := x_4, expr := Lean.Expr.fvar id' x, isBinder := true } => id' == id | x => false) t with | some i' => match Lean.Elab.Info.range? i' with | some r => let r := String.Range.toLspRange text r; let ll := { originSelectionRange? := (fun a => String.Range.toLspRange text a) <$> Lean.Elab.Info.range? i, targetUri := p.textDocument.uri, targetRange := r, targetSelectionRange := r }; pure #[ll] | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y let locationLinksFromImport : Lean.Elab.Info → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun i => let name := Lean.Syntax.getId (Lean.Syntax.getOp (Lean.Elab.Info.stx i) 2); do let a ← documentUriFromModule name let _do_jp : PUnit → Lean.MetaM (Array Lean.Lsp.LocationLink) := fun y => pure #[] match a with | some modUri => let range := { start := { line := 0, character := 0 }, end := { line := 0, character := 0 } }; let ll := { originSelectionRange? := none, targetUri := modUri, targetRange := range, targetSelectionRange := range }; pure #[ll] | x => do let y ← pure PUnit.unit _do_jp y Lean.Server.RequestM.withWaitFindSnap doc (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s > hoverPos)) (pure #[]) fun snap => let _do_jp := fun y => pure #[]; match Lean.Elab.InfoTree.hoverableInfoAt? (Lean.Server.Snapshots.Snapshot.infoTree snap) hoverPos with | some (ci, i) => let _do_jp := fun y => let _do_jp := fun y => let _do_jp := fun y => match Lean.Elab.Info.toElabInfo? i with | some ei => let _do_jp := fun y => if (kind == Lean.Server.FileWorker.GoToKind.definition && Lean.Environment.contains ci.env ei.elaborator) = true then do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromDecl i ei.elaborator)) pure a else do let y ← pure PUnit.unit _do_jp y; if (kind == Lean.Server.FileWorker.GoToKind.declaration && Lean.Environment.contains ci.env (Lean.Syntax.getKind ei.stx)) = true then do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromDecl i (Lean.Syntax.getKind ei.stx))) pure a else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y; match i with | Lean.Elab.Info.ofCommandInfo { toElabInfo := { elaborator := Lean.Name.str Lean.Name.anonymous "import" x_1, stx := x } } => if (kind == Lean.Server.FileWorker.GoToKind.definition || kind == Lean.Server.FileWorker.GoToKind.declaration) = true then do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromImport i)) pure a else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y; match i with | Lean.Elab.Info.ofFieldInfo fi => if (kind == Lean.Server.FileWorker.GoToKind.type) = true then do let expr ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) do let a ← Lean.Meta.inferType fi.val Lean.Meta.instantiateMVars a) match Lean.Expr.constName? (Lean.Expr.getAppFn expr) with | some n => do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromDecl i n)) pure a | x => do let y ← pure PUnit.unit _do_jp y else do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromDecl i fi.projName)) pure a | x => do let y ← pure PUnit.unit _do_jp y; match i with | Lean.Elab.Info.ofTermInfo ti => let expr := ti.expr; let _do_jp := fun expr y => match expr with | Lean.Expr.const n x x_1 => do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromDecl i n)) pure a | Lean.Expr.fvar id x => do let a ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (locationLinksFromBinder (Lean.Server.Snapshots.Snapshot.infoTree snap) i id)) pure a | x => do let y ← pure () _do_jp y; if (kind == Lean.Server.FileWorker.GoToKind.type) = true then do let r ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) do let a ← Lean.Meta.inferType expr let a ← Lean.Meta.instantiateMVars a pure (Lean.Expr.getAppFn a)) let expr : Lean.Expr := r let y ← pure PUnit.unit _do_jp expr y else do let y ← pure PUnit.unit _do_jp expr y | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Server.FileWorker.getInteractiveGoals p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let hoverPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.toTextDocumentPositionParams.position Lean.Server.RequestM.withWaitFindSnap doc (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s ≥ hoverPos)) (pure none) fun snap => match Lean.Elab.InfoTree.goalsAt? doc.meta.text (Lean.Server.Snapshots.Snapshot.infoTree snap) hoverPos with | rs@h:(x :: x_1) => do let goals ← List.join <$> List.mapM (fun x => match x with | { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } => let ci := if useAfter = true then { env := ci.env, fileMap := ci.fileMap, mctx := ti.mctxAfter, options := ci.options, currNamespace := ci.currNamespace, openDecls := ci.openDecls } else { env := ci.env, fileMap := ci.fileMap, mctx := ti.mctxBefore, options := ci.options, currNamespace := ci.currNamespace, openDecls := ci.openDecls }; let goals := if useAfter = true then ti.goalsAfter else ti.goalsBefore; liftM (Lean.Elab.ContextInfo.runMetaM ci { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } (List.mapM (fun g => Lean.Meta.withPPInaccessibleNames (Lean.Widget.goalToInteractive g)) goals))) rs pure (some { goals := List.toArray goals }) | x => pure none
Equations
- Lean.Server.FileWorker.handlePlainGoal p = do let t ← Lean.Server.FileWorker.getInteractiveGoals p pure (Task.map (Except.map (Option.map fun x => match x with | { goals := goals } => if Array.isEmpty goals = true then { rendered := "no goals", goals := #[] } else let goalStrs := Array.map (fun a => toString (Lean.Widget.InteractiveGoal.pretty a)) goals; let goalBlocks := Array.map (fun goal => toString "```lean\n" ++ toString goal ++ toString "\n```") goalStrs; let md := String.intercalate "\n---\n" (Array.toList goalBlocks); { rendered := md, goals := goalStrs })) t)
Equations
- Lean.Server.FileWorker.getInteractiveTermGoal p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let hoverPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.toTextDocumentPositionParams.position Lean.Server.RequestM.withWaitFindSnap doc (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s > hoverPos)) (pure none) fun snap => match Lean.Elab.InfoTree.termGoalAt? (Lean.Server.Snapshots.Snapshot.infoTree snap) hoverPos with | some (ci, i@h:(Lean.Elab.Info.ofTermInfo ti)) => do let ty ← liftM (Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) do let a ← Lean.Meta.inferType ti.expr Lean.Meta.instantiateMVars (Option.getD ti.expectedType? a)) let lctx' : Lean.LocalContext := if ti.isBinder = true then Lean.LocalContext.pop (Lean.Elab.Info.lctx i) else Lean.Elab.Info.lctx i let goal ← liftM (Lean.Elab.ContextInfo.runMetaM ci lctx' do let a ← Lean.Meta.mkFreshExprMVar (some ty) Lean.MetavarKind.natural Lean.Name.anonymous Lean.Meta.withPPInaccessibleNames (Lean.Widget.goalToInteractive (Lean.Expr.mvarId! a))) let range : Lean.Lsp.Range := match Lean.Elab.Info.range? i with | some r => String.Range.toLspRange text r | x => { start := p.toTextDocumentPositionParams.position, end := p.toTextDocumentPositionParams.position } pure (some { hyps := goal.hyps, type := goal.type, range := range }) | x => pure none
Equations
- Lean.Server.FileWorker.handlePlainTermGoal p = do let t ← Lean.Server.FileWorker.getInteractiveTermGoal p pure (Task.map (Except.map (Option.map fun goal => { goal := toString (Lean.Widget.InteractiveGoal.pretty (Lean.Widget.InteractiveTermGoal.toInteractiveGoal goal)), range := goal.range })) t)
Equations
- Lean.Server.FileWorker.handleDocumentHighlight p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let pos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.toTextDocumentPositionParams.position (fun highlightReturn? => let highlightRefs? := fun snaps pos => Id.run (let trees := Array.map (fun a => Lean.Server.Snapshots.Snapshot.infoTree a) snaps; let refs := Lean.Server.findModuleRefs text trees; do let discr ← Lean.Lsp.ModuleRefs.findAt? refs p.toTextDocumentPositionParams.position match discr with | some ident => do let discr ← Std.HashMap.find? refs ident match discr with | some info => let ranges := #[]; let _do_jp := fun ranges y => let ranges := Array.append ranges info.usages; some (Array.map (fun a => { range := a, kind? := some Lean.Lsp.DocumentHighlightKind.text }) ranges); match info.definition with | some definition => let ranges := Array.push ranges definition; do let y ← pure PUnit.unit _do_jp ranges y | x => do let y ← pure PUnit.unit _do_jp ranges y | x => none | x => none); Lean.Server.RequestM.withWaitFindSnap doc (fun s => decide (Lean.Server.Snapshots.Snapshot.endPos s > pos)) (pure #[]) fun snap => do let discr ← liftM (IO.AsyncList.updateFinishedPrefix (Lean.Server.FileWorker.EditableDocument.allSnaps doc)) let x : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot × Option Lean.Server.FileWorker.ElabTaskError := discr match x with | (snaps, x) => do let a ← pure (highlightRefs? (List.toArray (IO.AsyncList.finishedPrefix snaps)) p.toTextDocumentPositionParams.position) let _do_jp : PUnit → Lean.Server.RequestM (Array Lean.Lsp.DocumentHighlight) := fun y => let _do_jp := fun y => pure #[]; match highlightReturn? none snap.stx with | some hi => pure #[hi] | x => do let y ← pure PUnit.unit _do_jp y match a with | some his => pure his | x => do let y ← pure PUnit.unit _do_jp y) (Lean.Server.FileWorker.handleDocumentHighlight.highlightReturn? text pos)
partial def
Lean.Server.FileWorker.handleDocumentHighlight.highlightReturn?
(text : Lean.FileMap)
(pos : String.Pos)
(doRange? : Option Lean.Lsp.Range)
:
Equations
- Lean.Server.FileWorker.handleDocumentSymbol p = (fun toDocumentSymbols sectionLikeToDocumentSymbols => do let doc ← Lean.Server.RequestM.readDoc Lean.Server.RequestM.asTask do let discr ← liftM (IO.AsyncList.updateFinishedPrefix doc.cmdSnaps) let x : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot × Option Lean.Server.FileWorker.ElabTaskError := discr match x with | (cmdSnaps, e?) => let stxs := List.map (fun a => a.stx) (IO.AsyncList.finishedPrefix cmdSnaps); let _do_jp := fun stxs y => let lastSnap := List.getLastD (IO.AsyncList.finishedPrefix cmdSnaps) doc.headerSnap; do let a ← liftM (Lean.Server.Snapshots.parseAhead doc.meta.text.source lastSnap) let stxs : List Lean.Syntax := stxs ++ Array.toList a let x : List Lean.Lsp.DocumentSymbol × List Lean.Syntax := toDocumentSymbols doc.meta.text stxs match x with | (syms, x) => pure { syms := List.toArray syms }; match e? with | some Lean.Server.FileWorker.ElabTaskError.aborted => do let y ← throw Lean.Server.RequestError.fileChanged _do_jp stxs y | some (Lean.Server.FileWorker.ElabTaskError.ioError e) => do let y ← throw { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e } _do_jp stxs y | x => do let y ← pure () _do_jp stxs y) Lean.Server.FileWorker.handleDocumentSymbol.toDocumentSymbols Lean.Server.FileWorker.handleDocumentSymbol.sectionLikeToDocumentSymbols
partial def
Lean.Server.FileWorker.handleDocumentSymbol.sectionLikeToDocumentSymbols
(text : Lean.FileMap)
(stx : Lean.Syntax)
(stxs : List Lean.Syntax)
(name : String)
(kind : Lean.Lsp.SymbolKind)
(selection : Lean.Syntax)
:
Equations
- Lean.Server.FileWorker.noHighlightKinds = #[`Lean.Parser.Term.sorry, `Lean.Parser.Term.type, `Lean.Parser.Term.prop, `antiquotName, `Lean.Parser.Command.docComment]
- beginPos : String.Pos
- endPos : String.Pos
- text : Lean.FileMap
- snap : Lean.Server.Snapshots.Snapshot
- data : Array Nat
- lastLspPos : Lean.Lsp.Position
Equations
- Lean.Server.FileWorker.handleSemanticTokens beginPos endPos = (fun highlightKeyword addToken => do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let t ← liftM (IO.AsyncList.waitAll (fun a => decide (a.beginPos < endPos)) doc.cmdSnaps) Lean.Server.RequestM.mapTask t fun x => match x with | (snaps, x) => StateT.run' (do let r ← forIn snaps PUnit.unit fun s r => let _do_jp := fun y => do ReaderT.run (go s.stx) { beginPos := beginPos, endPos := endPos, text := text, snap := s } pure (ForInStep.yield PUnit.unit); if Lean.Server.Snapshots.Snapshot.endPos s ≤ beginPos then pure (ForInStep.yield PUnit.unit) else do let y ← pure PUnit.unit _do_jp y let x : PUnit := r let a ← get pure { data := a.data }) { data := #[], lastLspPos := { line := 0, character := 0 } }) Lean.Server.FileWorker.handleSemanticTokens.go Lean.Server.FileWorker.handleSemanticTokens.highlightId Lean.Server.FileWorker.handleSemanticTokens.highlightKeyword Lean.Server.FileWorker.handleSemanticTokens.addToken
Equations
- Lean.Server.FileWorker.handleSemanticTokens.highlightId stx = match Lean.Syntax.getRange? stx with | some range => let lastPos := range.start; do let a ← read let r ← let col := Lean.Elab.InfoTree.deepestNodes (fun x x_1 x_2 => match x, x_1, x_2 with | x, i@h:(Lean.Elab.Info.ofTermInfo ti), x_3 => match Lean.Elab.Info.pos? i with | some ipos => if String.Range.contains range ipos = true then some ti else none | x => none | x, x_3, x_4 => none) (Lean.Server.Snapshots.Snapshot.infoTree a.snap); forIn col lastPos fun ti r => let lastPos := r; let pos := Option.get! (Lean.Syntax.getPos? ti.toElabInfo.stx); let _do_jp := fun lastPos y => match ti.expr with | Lean.Expr.fvar x x_1 => do Lean.Server.FileWorker.handleSemanticTokens.addToken ti.toElabInfo.stx Lean.Lsp.SemanticTokenType.variable pure (ForInStep.yield lastPos) | x => if Option.get! (Lean.Syntax.getPos? ti.toElabInfo.stx) > lastPos then do Lean.Server.FileWorker.handleSemanticTokens.addToken ti.toElabInfo.stx Lean.Lsp.SemanticTokenType.property let lastPos : String.Pos := Option.get! (Lean.Syntax.getPos? ti.toElabInfo.stx) pure PUnit.unit pure (ForInStep.yield lastPos) else do pure PUnit.unit pure (ForInStep.yield lastPos); if pos < lastPos then pure (ForInStep.yield lastPos) else do let y ← pure PUnit.unit _do_jp lastPos y let x : String.Pos := r let lastPos : String.Pos := x pure PUnit.unit | x => pure PUnit.unit
Equations
- Lean.Server.FileWorker.handleSemanticTokens.highlightKeyword stx = match stx with | Lean.Syntax.atom info val => if (decide (String.length val > 0) && Char.isAlpha (String.getOp val 0) || decide (String.length val > 1) && String.getOp val 0 == Char.ofNat 35 && Char.isAlpha (String.getOp val 1)) = true then Lean.Server.FileWorker.handleSemanticTokens.addToken stx Lean.Lsp.SemanticTokenType.keyword else pure PUnit.unit | x => pure PUnit.unit
def
Lean.Server.FileWorker.handleSemanticTokens.addToken
(stx : Lean.Syntax)
(type : Lean.Lsp.SemanticTokenType)
:
Equations
- Lean.Server.FileWorker.handleSemanticTokens.addToken stx type = do let discr ← read let x : Lean.Server.FileWorker.SemanticTokensContext := discr match x with | { beginPos := beginPos, endPos := endPos, text := text, snap := x } => match (Lean.Syntax.getPos? stx, Lean.Syntax.getTailPos? stx) with | (some pos, some tailPos) => if (decide (beginPos ≤ pos) && decide (pos < endPos)) = true then do let a ← get let lspPos : Lean.Lsp.Position := a.lastLspPos let lspPos' : Lean.Lsp.Position := Lean.FileMap.utf8PosToLspPos text pos let deltaLine : Nat := lspPos'.line - lspPos.line let deltaStart : Nat := lspPos'.character - if (lspPos'.line == lspPos.line) = true then lspPos.character else 0 let length : Nat := (Lean.FileMap.utf8PosToLspPos text tailPos).character - lspPos'.character let tokenType : Nat := Lean.Lsp.SemanticTokenType.toNat type let tokenModifiers : Nat := 0 modify fun st => { data := st.data ++ #[deltaLine, deltaStart, length, tokenType, tokenModifiers], lastLspPos := lspPos' } else pure PUnit.unit | x => pure PUnit.unit
Equations
- Lean.Server.FileWorker.handleSemanticTokensRange p = do let doc ← Lean.Server.RequestM.readDoc let text : Lean.FileMap := doc.meta.text let beginPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.range.start let endPos : String.Pos := Lean.FileMap.lspPosToUtf8Pos text p.range.end Lean.Server.FileWorker.handleSemanticTokens beginPos endPos
Equations
- Lean.Server.FileWorker.handleWaitForDiagnostics p = (fun waitLoop => do let t ← Lean.Server.RequestM.asTask waitLoop Lean.Server.RequestM.bindTask t fun doc? => do let doc ← liftExcept doc? let t₁ ← liftM (IO.AsyncList.waitAll (fun x => true) doc.cmdSnaps) pure (Task.map (fun x => pure { } ) t₁)) (Lean.Server.FileWorker.handleWaitForDiagnostics.waitLoop p)