From fc5082eaef89cb0039aa63f82381b8ae08519a1f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 4 Nov 2021 14:43:25 +0100 Subject: [PATCH] perf: server: reset info trees for each snapshot --- src/Lean/Server/Snapshots.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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