Skip to content

Commit

Permalink
fix(frontends/lean/builtin_cmds): use correct end pos for #check et…
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Jul 13, 2022
1 parent 9dc6b1e commit 84516f9
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
8 changes: 4 additions & 4 deletions src/frontends/lean/builtin_cmds.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ environment check_cmd(parser & p, ast_id & cmd_id) {
// do not show useless type-checking results such as ?? : ?M_1
return p.env();
}
auto out = p.mk_message(data.m_start, p.pos(), INFORMATION);
auto out = p.mk_message(data.m_start, p.end_pos(), INFORMATION);
formatter fmt = out.get_formatter();
unsigned indent = get_pp_indent(p.get_options());
format e_fmt = fmt(e);
Expand Down Expand Up @@ -238,7 +238,7 @@ environment reduce_cmd(parser & p, ast_id & cmd_id) {
bool eta = false;
r = normalize(ctx, e, eta);
}
auto out = p.mk_message(data.m_start, p.pos(), INFORMATION);
auto out = p.mk_message(data.m_start, p.end_pos(), INFORMATION);
out.set_caption("reduce result") << r;
out.report();
return p.env();
Expand Down Expand Up @@ -493,7 +493,7 @@ static environment unify_cmd(parser & p, ast_id & cmd_id) {
local_context lctx;
e1 = convert_metavars(mctx, e1);
e2 = convert_metavars(mctx, e2);
auto rep = p.mk_message(data.m_start, p.pos(), INFORMATION);
auto rep = p.mk_message(data.m_start, p.end_pos(), INFORMATION);
rep << e1 << " =?= " << e2 << "\n";
type_context_old ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible);
bool success = ctx.is_def_eq(e1, e2);
Expand Down Expand Up @@ -551,7 +551,7 @@ static environment eval_cmd(parser & p, ast_id & cmd_id) {
name fn_name = "_main";
auto new_env = compile_expr(p.env(), p.get_options(), fn_name, ls, type, e, pos);

auto out = p.mk_message(data.m_start, p.pos(), INFORMATION);
auto out = p.mk_message(data.m_start, p.end_pos(), INFORMATION);
out.set_caption("eval result");
scope_traces_as_messages scope_traces(p.get_stream_name(), data.m_start);
bool should_report = false;
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/interactive/info_id_pre_elab.lean.expected.out
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","end_pos_col":27,"end_pos_line":7,"file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (tac.abstract none) : tactic unit → tactic unit"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","end_pos_col":16,"end_pos_line":6,"file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (tac.abstract none) : tactic unit → tactic unit"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"state":"⊢ ?m_1"},"response":"ok","seq_num":4}
{"record":{"full-id":"tactic.abstract","source":,"state":"⊢ tactic unit → tactic unit","type":"tactic unit → opt_param (option name) none → opt_param bool tt → tactic unit"},"response":"ok","seq_num":7}

0 comments on commit 84516f9

Please sign in to comment.