diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index 280eab4d8c..52b46c14c3 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -124,7 +124,7 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do let (output, _) ← IO.FS.withIsolatedStreams do EIO.toIO ioErrorFromEmpty do Elab.Command.catchExceptions - (Elab.Command.elabCommandTopLevel cmdStx) + (getResetInfoTrees *> Elab.Command.elabCommandTopLevel cmdStx) cmdCtx cmdStateRef let mut postCmdState ← cmdStateRef.get if !output.isEmpty then