call functions

Author: Paul-Lez

LeanUtils/Utils.lean

@@ -72,14 +72,17 @@ def extractInfoTrees (fileName : System.FilePath) : IO (FileMap × List InfoTree
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   if Lean.MessageLog.hasErrors messages then
     IO.println s!"Ran into errors while parsing the header of {fileName}"
+    MessageLog.printErrors messages
   -- TODO: do we need to specify the main module here?
   let (env, messages) ← processHeader header {} messages inputCtx
   if Lean.MessageLog.hasErrors messages then
     IO.println s!"Ran into errors whist processing the header of {fileName}"
+    MessageLog.printErrors messages
   let commandState := Command.mkState env messages
   let frontendState ← IO.processCommands inputCtx parserState commandState
   if Lean.MessageLog.hasErrors frontendState.commandState.messages then
     IO.println s!"Ran into errors whist processing the commands in {fileName}"
+    MessageLog.printErrors messages
   let fileMap := FileMap.ofString input
   return (fileMap, frontendState.commandState.infoState.trees.toList)