max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: print module name instead of file name

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-04 20:00:35 -07:00
parent 7f878eeb95
commit 5801e0e65a
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/Init/Util.lean
View file

@ -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)

3
src/frontends/lean/builtin_exprs.cpp
View file

@ -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);
}