Selecting a region with vimscript

Question

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?

Answer 1

The problem is this line: normal <ESC>

If :normal worked how you think it does, then it would immediately leave visual mode that you just entered with your previous line (so the fix is just to remove that line).

However, what that command actually does is emulate you typing: <ESC>, and the S command is what garbles your line, deleting the current line and entering insert mode.

If you need to include control characters in a :normal command, you can either enter them by typing e.g. Ctrl-VEsc, or you can build the command as a string and run it with :execute:

execute "normal! \<Esc>"

A couple of other points:

1. When writing Vimscript, you should add an exclamation point to :normal! in order to ensure that it performs the default behaviour (instead of following maps. This is like using the nore forms of the :map commands unless there's a good reason not to.

2. An alternative method instead of moving the cursor around would be to set the '> and '< marks with setpos(), and then enter visual mode afterwards with normal! gv.