diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index b2d685f525..3fc386e58c 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -172,8 +172,8 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou else pushGroup flb [{ i with f }] (gs' is) w >>= be w -def prettyM (f : Format) (w : Nat) [Monad m] [MonadPrettyFormat m] : m Unit := - be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0, activeTags := 0 }]}] +def prettyM (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit := + be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent, activeTags := 0 }]}] @[inline] def bracket (l : String) (f : Format) (r : String) : Format := group (nest l.length $ l ++ f ++ r) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 4d74369f0d..3e261db7c3 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -116,7 +116,12 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD | nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId | nCtx, _, withContext ctx d => formatAux nCtx ctx d | _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d - | nCtx, ctx, tagged _ d => formatAux nCtx ctx d + | nCtx, ctx, tagged t d => + if let Name.str cls "_traceCtx" _ := t then do + let d₁ ← formatAux nCtx ctx d + return f!"[{cls}] {d₁}" + else + formatAux nCtx ctx d | nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d | nCtx, ctx, compose d₁ d₂ => do let d₁ ← formatAux nCtx ctx d₁; let d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂ | nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index dcaed0cd86..67ae1512e9 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -91,7 +91,7 @@ private def addNode (oldTraces : PersistentArray TraceElem) (cls : Name) (ref : if traces.isEmpty then oldTraces else - let d := MessageData.tagged cls m!"[{cls}] {MessageData.node (traces.toArray.map fun elem => elem.msg)}" + let d := MessageData.tagged (cls ++ `_traceCtx) (MessageData.node (traces.toArray.map fun elem => elem.msg)) oldTraces.push { ref := ref, msg := d } private def getResetTraces : m (PersistentArray TraceElem) := do @@ -106,7 +106,7 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do let ref ← getRef let msg ← addMessageContext msg let msg := addTraceOptions msg - modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged cls m!"[{cls}] {msg}" } + modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged (cls ++ `_traceMsg) m!"[{cls}] {msg}" } where addTraceOptions : MessageData → MessageData | MessageData.withContext ctx msg => MessageData.withContext { ctx with opts := ctx.opts.setBool `pp.analyze false } msg diff --git a/src/Lean/Widget/Data.lean b/src/Lean/Widget/Data.lean index 6fe6bc8259..7cbf51a4d9 100644 --- a/src/Lean/Widget/Data.lean +++ b/src/Lean/Widget/Data.lean @@ -42,15 +42,12 @@ def pretty (g : InteractiveGoal) : String := end InteractiveGoal --- TODO -structure LazyTrace where - contents : String - deriving Inhabited, FromJson, ToJson +deriving instance RpcEncoding with { withRef := true } for MessageData inductive MsgEmbed where | expr : CodeWithInfos → MsgEmbed | goal : InteractiveGoal → MsgEmbed - | lazyTrace : LazyTrace → MsgEmbed + | lazyTrace : Nat → Name → WithRpcRef MessageData → MsgEmbed deriving Inhabited namespace MsgEmbed @@ -58,20 +55,20 @@ namespace MsgEmbed -- TODO(WN): `deriving RpcEncoding` for `inductive` private inductive RpcEncodingPacket where | expr : TaggedText Lsp.RpcRef → RpcEncodingPacket - | goal : Nat → RpcEncodingPacket - | lazyTrace : LazyTrace → RpcEncodingPacket + | goal : Nat → RpcEncodingPacket -- TODO + | lazyTrace : Nat → Name → Lsp.RpcRef → RpcEncodingPacket deriving Inhabited, FromJson, ToJson instance : RpcEncoding MsgEmbed RpcEncodingPacket where rpcEncode a := match a with - | expr t => return RpcEncodingPacket.expr (← rpcEncode t) - | goal t => return RpcEncodingPacket.goal 0 - | lazyTrace t => return RpcEncodingPacket.lazyTrace (← rpcEncode t) + | expr t => return RpcEncodingPacket.expr (← rpcEncode t) + | goal t => return RpcEncodingPacket.goal 0 + | lazyTrace col n t => return RpcEncodingPacket.lazyTrace col n (← rpcEncode t) rpcDecode a := match a with - | RpcEncodingPacket.expr t => return expr (← rpcDecode t) - | RpcEncodingPacket.goal t => return unreachable! - | RpcEncodingPacket.lazyTrace t => return lazyTrace (← rpcDecode t) + | RpcEncodingPacket.expr t => return expr (← rpcDecode t) + | RpcEncodingPacket.goal t => return unreachable! + | RpcEncodingPacket.lazyTrace col n t => return lazyTrace col n (← rpcDecode t) end MsgEmbed @@ -85,9 +82,9 @@ open MsgEmbed def pretty (msg : InteractiveMessage) : String := let tt : TaggedText MsgEmbed := msg.rewrite fun - | expr tt, _ => TaggedText.text tt.stripTags - | goal g, _ => TaggedText.text g.pretty - | lazyTrace t, _ => TaggedText.text t.contents + | expr tt, _ => TaggedText.text tt.stripTags + | goal g, _ => TaggedText.text g.pretty + | lazyTrace _ _ _, subTt => subTt tt.stripTags end InteractiveMessage diff --git a/src/Lean/Widget/ExprWithCtx.lean b/src/Lean/Widget/ExprWithCtx.lean index 570c1c6565..d467129586 100644 --- a/src/Lean/Widget/ExprWithCtx.lean +++ b/src/Lean/Widget/ExprWithCtx.lean @@ -84,12 +84,12 @@ def formatExplicitInfos (e : Expr) : MetaM (Format × Std.RBMap Nat Elab.Info co formatWithOpts e optsPerPos /-- Tags a pretty-printed `Expr` with infos from the delaborator. -/ -partial def tagExprInfos (ctx : Elab.ContextInfo) (lctx : LocalContext) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText Nat) +partial def tagExprInfos (ctx : Elab.ContextInfo) (lctx : LocalContext) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText (Nat × Nat)) : CodeWithInfos := go tt where - go (tt : TaggedText Nat) := - tt.rewrite fun n subTt => + go (tt : TaggedText (Nat × Nat)) := + tt.rewrite fun (n, _) subTt => match infos.find? n with | none => go subTt | some i => TaggedText.tag (WithRpcRef.mk { ctx, lctx, info := i }) (go subTt) @@ -101,7 +101,8 @@ def inferType (e : Expr) : MetaM ExprWithCtx := do options := ← getOptions currNamespace := ← getCurrNamespace openDecls := ← getOpenDecls - fileMap := arbitrary } + fileMap := arbitrary + } return { ctx, lctx := ← getLCtx, expr := e} def tagged (e : Expr) : MetaM CodeWithInfos := do @@ -113,7 +114,8 @@ def tagged (e : Expr) : MetaM CodeWithInfos := do options := ← getOptions currNamespace := ← getCurrNamespace openDecls := ← getOpenDecls - fileMap := arbitrary } + fileMap := arbitrary + } tagExprInfos ctx (← getLCtx) infos tt def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do @@ -125,7 +127,8 @@ def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do options := ← getOptions currNamespace := ← getCurrNamespace openDecls := ← getOpenDecls - fileMap := arbitrary } + fileMap := arbitrary + } tagExprInfos ctx (← getLCtx) infos tt builtin_initialize diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 564bf180a6..01ed95fe74 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -72,23 +72,26 @@ instance [RpcEncoding α β] : RpcEncoding (TaggedText α) (TaggedText β) where rpcDecode a := a.mapM rpcDecode private structure TaggedState where - out : TaggedText Nat := TaggedText.text "" - tagStack : List (Nat × TaggedText Nat) := [] - column : Nat := 0 + out : TaggedText (Nat × Nat) := TaggedText.text "" + tagStack : List (Nat × Nat × TaggedText (Nat × Nat)) := [] + column : Nat := 0 deriving Inhabited instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where pushOutput s := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩ pushNewline indent := modify fun ⟨out, ts, col⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩ currColumn := return (←get).column - startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, out) :: ts, col⟩ + startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩ endTags n := modify fun ⟨out, ts, col⟩ => let (ended, left) := (ts.take n, ts.drop n) - let out' := ended.foldl (init := out) fun acc (n, top) => top.appendTag n acc + let out' := ended.foldl (init := out) fun acc (n, col', top) => top.appendTag (n, col') acc ⟨out', left, col⟩ -def prettyTagged (f : Format) (w : Nat := Std.Format.defWidth) : TaggedText Nat := - (f.prettyM w : StateM TaggedState Unit) {} |>.snd.out +/-- The output is tagged with `(tag, indent)` where `tag` is from the input `Format` and `indent` +is the indentation level at this point. The latter is used to print sub-trees accurately by passing +it again as the `indent` argument. -/ +def prettyTagged (f : Format) (indent := 0) (w : Nat := Std.Format.defWidth) : TaggedText (Nat × Nat) := + (f.prettyM w indent : StateM TaggedState Unit) {} |>.snd.out /-- Remove tags, leaving just the pretty-printed string. -/ partial def stripTags (tt : TaggedText α) : String :=