michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean): save 'choice' position

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 08:50:44 -07:00
parent 6085a54416
commit 656bcd55ed
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/calc.cpp
View file

@ -317,6 +317,6 @@ expr parse_calc(parser & p) {
buffer<expr> choices; buffer<expr> choices;
for (auto const & s : steps) for (auto const & s : steps)
choices.push_back(step_proof(s)); choices.push_back(step_proof(s));
return mk_choice(choices.size(), choices.data()); return p.save_pos(mk_choice(choices.size(), choices.data()), pos);
} }
} }

2
src/frontends/lean/parser.cpp
View file

@ -803,7 +803,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
expr r = instantiate_rev(copy_with_new_pos(a, p), args.size(), args.data()); expr r = instantiate_rev(copy_with_new_pos(a, p), args.size(), args.data());
cs.push_back(r); cs.push_back(r);
} }
return mk_choice(cs.size(), cs.data()); return save_pos(mk_choice(cs.size(), cs.data()), p);
} }
expr parser::parse_nud_notation() { expr parser::parse_nud_notation() {