max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove traceCtx

Browse source
This commit is contained in:
Gabriel Ebner 2022-08-07 17:35:17 +02:00 • committed by Leonardo de Moura
parent 0e8c05134f
commit 5e4b30c777
1 changed files with 0 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Util/Trace.lean
View file

@ -65,14 +65,6 @@ def isTracingEnabledFor (cls : Name) : m Bool := do
@[inline] def setTraceState (s : TraceState) : m Unit :=
modifyTraceState fun _ => s
private def addNode (oldTraces : PersistentArray TraceElem) (cls : Name) (ref : Syntax) : m Unit :=
modifyTraces fun traces =>
if traces.isEmpty then
oldTraces
else
let d := .trace cls "" (traces.toArray.map fun elem => elem.msg) (collapsed := true)
oldTraces.push { ref := ref, msg := d }
private def getResetTraces : m (PersistentArray TraceElem) := do
let oldTraces ← getTraces
modifyTraces fun _ => {}
@ -100,15 +92,6 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
let msg ← mkMsg
addTrace cls msg
@[inline] def traceCtx [MonadFinally m] (cls : Name) (ctx : m α) : m α := do
let b ← isTracingEnabledFor cls
if !b then
ctx
else
let ref ← getRef
let oldCurrTraces ← getResetTraces
try ctx finally addNode oldCurrTraces cls ref
private def addTraceNode (oldTraces : PersistentArray TraceElem)
(cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
withRef ref do