From 028c31779d958eb77f266bc9c4754a50f99334c4 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 15 Jun 2017 16:53:30 +0200 Subject: [PATCH] fix(frontends/lean/interactive): revert hole end column I have tested this change in both emacs and vscode, and replacements work correctly. This reverts commit 6c2a1449502dacc2d2f8568390af3d58bf6a1b7c. --- src/frontends/lean/interactive.cpp | 4 ++-- tests/lean/interactive/hole1.lean.expected.out | 2 +- tests/lean/interactive/hole2.lean.expected.out | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 81bedb9e7c..23beb144ed 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -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; } } diff --git a/tests/lean/interactive/hole1.lean.expected.out b/tests/lean/interactive/hole1.lean.expected.out index 1b7f19b310..dfbaed564c 100644 --- a/tests/lean/interactive/hole1.lean.expected.out +++ b/tests/lean/interactive/hole1.lean.expected.out @@ -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} diff --git a/tests/lean/interactive/hole2.lean.expected.out b/tests/lean/interactive/hole2.lean.expected.out index 57d535ea3f..7562a2da73 100644 --- a/tests/lean/interactive/hole2.lean.expected.out +++ b/tests/lean/interactive/hole2.lean.expected.out @@ -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}}