Skip to content

Commit cc50ca5

Browse files
Fix v4.22.0-rc2
1 parent 46fb3c5 commit cc50ca5

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

REPL/Frontend.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,15 +27,15 @@ where
2727
|>.foldl (· ++ ·) {}
2828
-- In contrast to messages, we should collect info trees only from the top-level command
2929
-- snapshots as they subsume any info trees reported incrementally by their children.
30-
let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
30+
let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
3131
let result : (IncrementalState × Option InfoTree) :=
32-
({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees }
32+
({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees }
3333
, parserState := snap.parserState
3434
, cmdPos := snap.parserState.pos
3535
, commands := commands.map (·.stx)
3636
, inputCtx := inputCtx
3737
, initialSnap := initialSnap
38-
}, snap.infoTreeSnap.get.infoTree?)
38+
}, snap.elabSnap.infoTreeSnap.get.infoTree?)
3939
if let some next := snap.nextCmdSnap? then
4040
result :: go initialSnap next.task commands
4141
else

0 commit comments

Comments
 (0)