Permalink
Browse files

fix a bug in Vimhol tactic expansion

If the visually selected tactic was indented and folding was on, the
call sent to HOL was empty. New version of HOLExpand() that is maybe
simpler (because that's where I thought the problem was originally), and
new version of HOLCStart() turns off folding in the temporary buffer.
  • Loading branch information...
1 parent 5a18cdc commit a4d2b6a54756ca20573871a02c33e6d31a17159e @xrchz xrchz committed Dec 29, 2012
Showing with 5 additions and 4 deletions.
  1. +5 −4 tools/vim/hol.src
View
@@ -25,6 +25,7 @@ fu! HOLCStart()
let s:prev = bufnr("")
let s:wins = winsaveview()
silent exe "keepjumps hide bu" s:holnr
+ setlocal foldmethod=manual
keepjumps %d_
endf
@@ -107,11 +108,11 @@ fu! HOLExpand()
while search('\%^\_s*\%(\%('.s:stripBoth.'\|'.s:stripStart.'\)\|\%('.s:stripBothWords.'\)\ze'.s:delim.'\)','cWe')
silent keepjumps normal vgg0"_d
endw
- keepjumps normal G$a)
- while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*)\%$','bW')
- silent keepjumps normal vG$"_dG$a)
+ while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*\%$','cW')
+ silent keepjumps normal vG$"_dgg0
endw
- keepjumps normal gg0iproofManagerLib.expand(
+ keepjumps normal iproofManagerLib.expand(
+ keepjumps normal G$a)
endf
fu! HOLSubgoal()

0 comments on commit a4d2b6a

Please sign in to comment.