From 9d61f1506d2a9220724b926a90edc7c86de82586 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= <kripnermatej@gmail.com>
Date: Wed, 17 Dec 2025 16:08:28 +0100
Subject: [PATCH] feat: report errors in import statements

---
 REPL/Frontend.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 81575ed3..f8e70a59 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -19,8 +19,9 @@ def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
+  let oldMessages := commandState.messages.toList
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  pure (s, oldMessages ++ s.messages.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.