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

fix(frontends/lean/interactive): revert hole end column

Browse source 
I have tested this change in both emacs and vscode, and replacements
work correctly.

This reverts commit 6c2a144950.
This commit is contained in:
Gabriel Ebner 2017-06-15 16:53:30 +02:00
parent e99786afcd
commit 028c31779d
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/interactive.cpp
View file

@ -277,7 +277,7 @@ bool json_of_hole(hole_info_data const & hole, std::string const & file, json &
j["start"]["line"] = hole.get_begin_pos().first;
j["start"]["column"] = hole.get_begin_pos().second;
j["end"]["line"] = hole.get_end_pos().first;
j["end"]["column"] = hole.get_end_pos().second + 1;
j["end"]["column"] = hole.get_end_pos().second;
return true;
}
@ -332,7 +332,7 @@ void execute_hole_command(module_info const & m_mod_info,
j["replacements"]["start"]["line"] = hole.get_begin_pos().first;
j["replacements"]["start"]["column"] = hole.get_begin_pos().second;
j["replacements"]["end"]["line"] = hole.get_end_pos().first;
j["replacements"]["end"]["column"] = hole.get_end_pos().second + 1;
j["replacements"]["end"]["column"] = hole.get_end_pos().second;
}
}

2
tests/lean/interactive/hole1.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"replacements":{"alternatives":[{"code":"a + a","description":""}],"end":{"column":17,"line":2},"file":"f","start":{"column":5,"line":2}},"response":"ok","seq_num":3}
{"replacements":{"alternatives":[{"code":"a + a","description":""}],"end":{"column":16,"line":2},"file":"f","start":{"column":5,"line":2}},"response":"ok","seq_num":3}

2
tests/lean/interactive/hole2.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"end":{"column":17,"line":2},"file":"f","response":"ok","results":[{"description":"Infer type of the expression in the hole","name":"Infer"},{"description":"Show the current goal","name":"Show"},{"description":"Try to fill the hole using the given argument","name":"Use"}],"seq_num":3,"start":{"column":5,"line":2}}
{"end":{"column":16,"line":2},"file":"f","response":"ok","results":[{"description":"Infer type of the expression in the hole","name":"Infer"},{"description":"Show the current goal","name":"Show"},{"description":"Try to fill the hole using the given argument","name":"Use"}],"seq_num":3,"start":{"column":5,"line":2}}