From 6abc8bb76997c1f15a77e2025766460ae6fe8188 Mon Sep 17 00:00:00 2001 From: Henrik Date: Sun, 10 Sep 2023 01:02:52 +0200 Subject: [PATCH] feat: print location of errors during documentation --- DocGen4/Process/Analyze.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index b071997..9c4c03d 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -134,7 +134,11 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do let module := res.find! moduleName res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)} catch e => - IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}" + if let some pos := e.getRef.getPos? then + let pos := (← getFileMap).toPosition pos + IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}" + else + IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}" -- TODO: This could probably be faster if we did sorted insert above instead for (moduleName, module) in res.toArray do