[vim-mode] add support for Proof modifiers

Handle things like `Proof[exclude_simps thms]` as follows:

- `ha` previously selected a goal-statement in between
  `Theorem`/`Triviality` and `Proof`. Now it also selects the `Proof`
  keyword and associated `[...]` (including over multiple lines).

- To help `ha` above, modify the `HOLSelect` function so that it opens
  any folds found at the endpoint of its selection.

- `hG` goal-setting command now invokes `proofManagerLib.new_goalstack`
  and `BasicProvers.mk_tacmod` as suggested by @mn200. It searches the
  selected "goal" for the `Proof` keyword to pass the correct bit to
  `mk_tacmod`. It remains compatible with selections which do not
  include the `Proof` keyword.

- `he` tactic expansion is eta-expanded so that the `Proof` modifier can
  intervene for calls to e.g. `srw_ss()` (suggsted by @mn200).

tools/vim/README.md

@@ -80,7 +80,7 @@ Command  | Description
 `hL`     | Send region to be split into words and each word `load`ed.
 `hl`     | Same as above, but also send the region as a command afterwards.
 `hg`     | Send region (should be a quotation) to `g`, to start a new proof.
-`hG`     | Send region to g after quoting it, to start a new proof.
+`hG`     | Send region to `new_goalstack` after quoting it, to start a new proof. Any trailing `Proof[...]` modifiers are passed to HOL too.
 `he`     | Send region (should be a tactic) to `e`, to expand a tactic.
 `hS`     | Send region (should be a quotation) as a new subgoal.
 `hF`     | Send region (should be a quotation) to be proved sufficient then proved.
@@ -103,7 +103,7 @@ Command     | Description
 `hc`        | Interrupt execution (of whichever of the things sent is running).
 `ht`        | Select a quotation, including the  `` ` `` delimiters. Find `` ` `` left of (or under) cursor and select to next `` ` ``.  Also works for Unicode single quotes (`‘` and `’`).
 `hT`        | Select a term: same as above, but with ``` `` ``` delimiters. (Or Unicode `“` and `”`.)
-`ha`        | Select the previous (or if within current) Theorem or Trivialty statement.
+`ha`        | Select the previous (or if within current) `Theorem` or `Triviality` statement, including its `Proof` keyword and associated modifiers.
 `hh`        | A normal h (usually means move cursor left). This one works in both normal and visual modes.
 `hy`        | Toggle HOL's show types trace.
 `hn`        | Toggle HOL's `PP.avoid_unicode` trace.

tools/vim/hol.src

@@ -111,8 +111,15 @@ fu! HOLGoal()
 endf
 
 fu! HOLUQGoal()
-  silent keepjumps normal pG$a`)
-  silent keepjumps normal gg0iproofManagerLib.g(`
+  silent keepjumps normal pG
+  if search('^Proof','cbW')
+    silent keepjumps normal I``) (BasicProvers.mk_tacmod "
+    silent keepjumps normal VGJ
+    silent keepjumps normal A") I
+  else
+    silent keepjumps normal GA``) (BasicProvers.mk_tacmod "Proof") I
+  endif
+  silent keepjumps normal gg0iproofManagerLib.new_goalstack([],``
 endf
 
 let s:stripStart     = ')\|\]\|\['
@@ -129,8 +136,8 @@ fu! HOLExpand()
   while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*\%$','cW')
     silent keepjumps normal vG$"_dgg0
   endw
-  keepjumps normal iproofManagerLib.expand(
-  keepjumps normal G$a)
+  keepjumps normal iproofManagerLib.expand(fn HOLgoal => (
+  keepjumps normal G$a) HOLgoal)
 endf
 
 fu! HOLSubgoal()
@@ -197,6 +204,7 @@ fu! HOLSelect(l,r)
     return
   endif
   call search(a:r,"ce")
+  normal zv
 endf
 
 fu! HOLPattern()
@@ -244,7 +252,7 @@ nn <buffer><silent> <LocalLeader>r :call HOLCall(function("HOLF"),["proofManager
 nn <buffer><silent> <LocalLeader>c :call HOLINT()<CR>
 nn <buffer><silent> <LocalLeader>t :call HOLSelect('`\\|‘','`\\|’')<CR>
 nn <buffer><silent> <LocalLeader>T :call HOLSelect('``\\|“','``\\|”')<CR>
-nn <buffer><silent> <LocalLeader>a :call HOLSelect('^Triviality\\|^Theorem','^Proof')<CR>-Vo+
+nn <buffer><silent> <LocalLeader>a :call HOLSelect('^Triviality\\|^Theorem','^Proof$\\|^Proof\[\_.\{-}\]')<CR>Vo+
 nn <buffer><silent> <LocalLeader>y :call HOLCall(function("HOLF"),["Globals.show_types:=not(!Globals.show_types)"])<CR>
 nn <buffer><silent> <LocalLeader>n :call HOLCall(function("HOLF"),["Feedback.set_trace \"PP.avoid_unicode\" (1 - Feedback.current_trace \"PP.avoid_unicode\")"])<CR>
 no <buffer><LocalLeader>h h