Equations
- Lean.Widget.Lean.MessageData.instRpcEncodingWithRpcRefMessageDataRpcRef = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => [anonymous], rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => [anonymous] }
- expr: Lean.Widget.CodeWithInfos → Lean.Widget.MsgEmbed
- goal: Lean.Widget.InteractiveGoal → Lean.Widget.MsgEmbed
- lazyTrace: Nat → Lean.Name → Lean.Server.WithRpcRef Lean.MessageData → Lean.Widget.MsgEmbed
Equations
- Lean.Widget.instInhabitedMsgEmbed = { default := Lean.Widget.MsgEmbed.expr default }
noncomputable def
Lean.Widget.MsgEmbed.rpcPacketFor
{β : outParam Type}
(α : Type)
[inst : Lean.Server.RpcEncoding α β]
:
outParam Type
Equations
Equations
- Lean.Widget.MsgEmbed.instToJsonRpcEncodingPacket = { toJson := [anonymous] }
Equations
- Lean.Widget.MsgEmbed.instInhabitedRpcEncodingPacket = { default := Lean.Widget.MsgEmbed.RpcEncodingPacket.expr default }
Equations
- Lean.Widget.MsgEmbed.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }
Equations
- Lean.Widget.MsgEmbed.instRpcEncodingMsgEmbedRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => match a with | Lean.Widget.MsgEmbed.expr t => do let a ← Lean.Server.rpcEncode t pure (Lean.Widget.MsgEmbed.RpcEncodingPacket.expr a) | Lean.Widget.MsgEmbed.goal g => do let a ← Lean.Server.rpcEncode g pure (Lean.Widget.MsgEmbed.RpcEncodingPacket.goal a) | Lean.Widget.MsgEmbed.lazyTrace col n t => do let a ← Lean.Server.rpcEncode t pure (Lean.Widget.MsgEmbed.RpcEncodingPacket.lazyTrace col n a), rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => match a with | Lean.Widget.MsgEmbed.RpcEncodingPacket.expr t => do let a ← Lean.Server.rpcDecode t pure (Lean.Widget.MsgEmbed.expr a) | Lean.Widget.MsgEmbed.RpcEncodingPacket.goal g => do let a ← Lean.Server.rpcDecode g pure (Lean.Widget.MsgEmbed.goal a) | Lean.Widget.MsgEmbed.RpcEncodingPacket.lazyTrace col n t => do let a ← Lean.Server.rpcDecode t pure (Lean.Widget.MsgEmbed.lazyTrace col n a) }
@[inline]
Equations
- Lean.Widget.InteractiveDiagnostic.instRpcEncodingInteractiveDiagnosticRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.message pure { range := a.range, fullRange := a.fullRange, severity? := a.severity?, code? := a.code?, source? := a.source?, message := a_1, tags? := a.tags?, relatedInformation? := a.relatedInformation? }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.message pure { range := a.range, fullRange := a.fullRange, severity? := a.severity?, code? := a.code?, source? := a.source?, message := a_1, tags? := a.tags?, relatedInformation? := a.relatedInformation? } }
Equations
- Lean.Widget.InteractiveDiagnostic.toDiagnostic diag = (fun prettyTt => { range := diag.range, fullRange := diag.fullRange, severity? := diag.severity?, code? := diag.code?, source? := diag.source?, message := prettyTt diag.message, tags? := diag.tags?, relatedInformation? := diag.relatedInformation? }) Lean.Widget.InteractiveDiagnostic.toDiagnostic.prettyTt
def
Lean.Widget.InteractiveDiagnostic.toDiagnostic.prettyTt
(tt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed)
:
Equations
- Lean.Widget.InteractiveDiagnostic.toDiagnostic.prettyTt tt = let tt := Lean.Widget.TaggedText.rewrite (fun x x_1 => match x, x_1 with | Lean.Widget.MsgEmbed.expr tt, x => Lean.Widget.TaggedText.text (Lean.Widget.TaggedText.stripTags tt) | Lean.Widget.MsgEmbed.goal g, x => Lean.Widget.TaggedText.text (toString (Lean.Widget.InteractiveGoal.pretty g)) | Lean.Widget.MsgEmbed.lazyTrace x x_2 x_3, subTt => subTt) tt; Lean.Widget.TaggedText.stripTags tt
Equations
- Lean.Widget.instInhabitedEmbedFmt = { default := Lean.Widget.EmbedFmt.goal default default default }
def
Lean.Widget.msgToInteractive
(msgData : Lean.MessageData)
(hasWidgets : Bool)
(indent : optParam Nat 0)
:
Equations
- Lean.Widget.msgToInteractive msgData hasWidgets indent = do let discr ← Lean.Widget.msgToInteractiveAux msgData hasWidgets let x : Lean.Format × Array Lean.Widget.EmbedFmt := discr match x with | (fmt, embeds) => let tt := Lean.Widget.TaggedText.prettyTagged fmt indent; Lean.Widget.TaggedText.rewriteM (fun x subTt => match x with | (n, col) => match Array.get! embeds n with | Lean.Widget.EmbedFmt.expr ctx infos => let subTt' := Lean.Widget.tagExprInfos ctx infos subTt; pure (Lean.Widget.TaggedText.tag (Lean.Widget.MsgEmbed.expr subTt') (Lean.Widget.TaggedText.text (Lean.Widget.TaggedText.stripTags subTt))) | Lean.Widget.EmbedFmt.goal ctx lctx g => panicWithPosWithDecl "Lean.Widget.InteractiveDiagnostic" "Lean.Widget.msgToInteractive" 171 6 "unreachable code has been reached" | Lean.Widget.EmbedFmt.lazyTrace nCtx ctx? cls m => let msg := match ctx? with | some ctx => Lean.MessageData.withNamingContext nCtx (Lean.MessageData.withContext ctx m) | none => Lean.MessageData.withNamingContext nCtx m; pure (Lean.Widget.TaggedText.tag (Lean.Widget.MsgEmbed.lazyTrace col cls { val := msg }) (Lean.Widget.TaggedText.text (Lean.Widget.TaggedText.stripTags subTt))) | Lean.Widget.EmbedFmt.ignoreTags => pure (Lean.Widget.TaggedText.text (Lean.Widget.TaggedText.stripTags subTt))) tt
def
Lean.Widget.msgToInteractiveDiagnostic
(text : Lean.FileMap)
(m : Lean.Message)
(hasWidgets : Bool)
:
Equations
- Lean.Widget.msgToInteractiveDiagnostic text m hasWidgets = let low := Lean.FileMap.leanPosToLspPos text m.pos; let fullHigh := Lean.FileMap.leanPosToLspPos text (Option.getD m.endPos m.pos); let high := match m.endPos with | some endPos => let endPos := if endPos.line > m.pos.line then { line := m.pos.line + 1, column := 0 } else endPos; Lean.FileMap.leanPosToLspPos text endPos | none => low; let range := { start := low, end := high }; let fullRange := { start := low, end := fullHigh }; let severity := match m.severity with | Lean.MessageSeverity.information => some Lean.Lsp.DiagnosticSeverity.information | Lean.MessageSeverity.warning => some Lean.Lsp.DiagnosticSeverity.warning | Lean.MessageSeverity.error => some Lean.Lsp.DiagnosticSeverity.error; let source := "Lean 4"; let _do_jp := fun message => pure { range := range, fullRange := fullRange, severity? := severity, code? := none, source? := some source, message := message, tags? := none, relatedInformation? := none }; do let y ← tryCatch (Lean.Widget.msgToInteractive m.data hasWidgets 0) fun ex => pure (Lean.Widget.TaggedText.text (toString "[error when printing message: " ++ toString (IO.Error.toString ex) ++ toString "]")) _do_jp y