From 93ceafbe805801fe5e56b9266ecfb15208e1e8d9 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" <alex.j.best@gmail.com> Date: Thu, 4 Jan 2024 02:35:13 +0000 Subject: [PATCH] fix --- Leaff/Diff.lean | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean index ea266c0..66713cc 100644 --- a/Leaff/Diff.lean +++ b/Leaff/Diff.lean @@ -673,15 +673,12 @@ def summarizeDiffImports (oldImports newImports : Array Import) (old new : Searc searchPathRef.set old let opts := Options.empty let trustLevel := 1024 -- TODO actually think about this value - try - withImportModules oldImports opts trustLevel fun oldEnv => do - -- TODO could be really clever here instead of passing search paths around and try and swap the envs in place - -- to reduce the need for multiple checkouts, but that seems complicated - searchPathRef.set new - withImportModules newImports opts trustLevel fun newEnv => do - IO.println <| ← (Diff.summarize (← oldEnv.diff newEnv)).format - catch ex => do - throw <| IO.userError s!"Exception: {← ex.toMessageData.toString}" + withImportModules oldImports opts trustLevel fun oldEnv => do + -- TODO could be really clever here instead of passing search paths around and try and swap the envs in place + -- to reduce the need for multiple checkouts, but that seems complicated + searchPathRef.set new + withImportModules newImports opts trustLevel fun newEnv => do + IO.println <| ← (Diff.summarize (← oldEnv.diff newEnv)).format section cmd