From 5801e0e65a0648769427bf53c3e9236befbcb0c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Oct 2019 20:00:35 -0700 Subject: [PATCH] fix: print module name instead of file name --- library/Init/Util.lean | 4 ++-- src/frontends/lean/builtin_exprs.cpp | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/library/Init/Util.lean b/library/Init/Util.lean index bf5f69e110..6347351bf3 100644 --- a/library/Init/Util.lean +++ b/library/Init/Util.lean @@ -29,5 +29,5 @@ unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β : constant panic {α : Type u} [Inhabited α] (msg : String) : α := default _ @[neverExtract] -def panicWithPos {α : Type u} [Inhabited α] (fname : String) (line col : Nat) (msg : String) : α := -panic ("PANIC at " ++ fname ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg) +def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α := +panic ("PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index ae65771200..72faea3e44 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -802,7 +802,8 @@ static expr parse_tparser(parser & p, unsigned, expr const *, pos_info const & p static expr parse_panic(parser & p, unsigned, expr const *, pos_info const & pos) { expr e = p.parse_expr(); - expr r = mk_app(mk_constant(get_panic_with_pos_name()), quote(p.get_file_name()), quote(pos.first), quote(pos.second), e); + std::string mod = p.env().get_main_module().to_string(); + expr r = mk_app(mk_constant(get_panic_with_pos_name()), quote(mod.c_str()), quote(pos.first), quote(pos.second), e); return save_pos(r, pos); }