- msg : Lean.Server.WithRpcRef Lean.MessageData
- indent : Nat
instance
Lean.Widget.Lean.Widget.MsgToInteractive.instRpcEncodingMsgToInteractiveRpcEncodingPacket
:
Equations
- Lean.Widget.Lean.Widget.MsgToInteractive.instRpcEncodingMsgToInteractiveRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.msg let a ← Lean.Server.rpcEncode a.indent pure { msg := a_1, indent := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.msg let a ← Lean.Server.rpcDecode a.indent pure { msg := a_1, indent := a } }
Equations
- Lean.Widget.instInhabitedMsgToInteractive = { default := { msg := default, indent := default } }
- type : Option Lean.Widget.CodeWithInfos
- exprExplicit : Option Lean.Widget.CodeWithInfos
- doc : Option String
Equations
- Lean.Widget.Lean.Widget.InfoPopup.instRpcEncodingInfoPopupRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.type let a_2 ← Lean.Server.rpcEncode a.exprExplicit let a ← Lean.Server.rpcEncode a.doc pure { type := a_1, exprExplicit := a_2, doc := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.type let a_2 ← Lean.Server.rpcDecode a.exprExplicit let a ← Lean.Server.rpcDecode a.doc pure { type := a_1, exprExplicit := a_2, doc := a } }
Equations
- Lean.Widget.instInhabitedInfoPopup = { default := { type := default, exprExplicit := default, doc := default } }
- lineRange? : Option Lean.Lsp.LineRange
Equations
- Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams = { default := { lineRange? := default } }
Equations
- Lean.Widget.getInteractiveDiagnostics params = do let doc ← Lean.Server.RequestM.readDoc let rangeEnd ← pure (Option.map (fun range => Lean.FileMap.lspPosToUtf8Pos doc.meta.text { line := range.end, character := 0 }) params.lineRange?) let t ← liftM (IO.AsyncList.waitAll (fun snap => Option.all (fun a => decide (snap.beginPos < a)) rangeEnd) doc.cmdSnaps) pure (Task.map (fun x => match x with | (snaps, x) => let diags? := Option.map (fun snap => pure (Array.filter (fun diag => Option.all (fun x => match x with | { start := s, end := e } => decide (s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨ diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line)) params.lineRange?) (Std.PersistentArray.toArray snap.interactiveDiags) 0 (Array.size (Std.PersistentArray.toArray snap.interactiveDiags)))) (List.getLast? snaps); Option.getD diags? (pure #[])) t)