This is a follow-up to Understanding a vimscript function
The file format is:
Theorem ∀ P. P ==> P Proof rw  \\ metis 
I modified that vimscript function:
fu! HOLSelectTactic() let l:cursor = getpos(".") if search("Proof","Wbc") == 0 return endif normal v normal <ESC> call setpos('.', l:cursor) return endf
with the following thought in mind: select the region visually from Proof (search("Proof"...)) that is before the cursor
to the cursor (setpos('.' ...)). The command definition is
nn <silent> <LocalLeader>E :call HOLSelectTactic()<CR>Vo+
this with the following thought: select visually by line (capital V), go to the other end of the selection (Proof) and come down one line.
In theory, this would select the two lines after Proof when the cursor is at the end.
In practice, is selects only the metis line, and garbles the Proof line. I really do not understand how it could alter the file.
What is the bug in my code and how can I fix it?