From b29450b1127ac9377a27a33bce068ade7e468cd9 Mon Sep 17 00:00:00 2001 From: Jonathan Sailor Date: Wed, 30 Jan 2013 23:04:27 -0500 Subject: [PATCH 1/4] Make it easier to turn debugging on/off --- plugin/coq_IDE.vim | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugin/coq_IDE.vim b/plugin/coq_IDE.vim index af1644b..3f7a419 100644 --- a/plugin/coq_IDE.vim +++ b/plugin/coq_IDE.vim @@ -120,12 +120,14 @@ let s:refreshcount = 100 " When processing a bunch of commands refresh the scree " Global definitions function s:Debug(category, msg) + if 0 + "if a:category == 'infonextdot' "if a:category == 'UpdateColor' "if a:category == 'NextPosN' "if a:category == 'info_undo' "if a:category == 'info_history' || a:category == 'info_undo' - " echomsg a:msg - "endif + echomsg a:msg + endif endfunction """"""""""""""""""""""""""""""" From 7bd71a8950e5fcd1f9ee7fdec206fa22aeb71fdd Mon Sep 17 00:00:00 2001 From: Jonathan Sailor Date: Wed, 30 Jan 2013 23:05:27 -0500 Subject: [PATCH 2/4] Rewrite most of s:GetNextCmd(). Fix some '.' bugs. In particular, be aware that dots in strings don't end commands, and aware that dots in ".." (e.g. when defining Notation) don't end commands either. --- plugin/coq_IDE.vim | 66 ++++++++++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 28 deletions(-) diff --git a/plugin/coq_IDE.vim b/plugin/coq_IDE.vim index 3f7a419..347b21b 100644 --- a/plugin/coq_IDE.vim +++ b/plugin/coq_IDE.vim @@ -915,47 +915,57 @@ function s:GetNextCmd() return [GetPart(b:curline, b:curcol, l:dline, l:dcol + 1), l:dline, l:dcol + 1, 0] endif - " Then Search for a '.' outside comments - let l:found = 0 - let l:eof = 0 - let l:dline = l:npl - let l:dcol = l:npc - - if getline(l:dline, l:dline) == [] - let l:eof = 1 + if getline(l:npl, l:npl) == [] + throw "eof" endif - while(! (l:found || l:eof)) - call cursor(l:dline, l:dcol) - let [l:cline, l:ccol] = searchpos('(\*', 'cW') - let [l:dline, l:dcol] = s:NextDot(l:dline, l:dcol) - - call s:Debug('infonextdot', '"(*" found at ' . l:cline . ', ' . l:ccol) - call s:Debug('infonextdot', '"." found at ' . l:dline . ', ' . l:dcol) + " Then Search for a '.' outside comments - if l:dline == 0 && l:dcol == 0 - let l:eof = 1 " Could be either EOF or the last command has no '.' at its end. - endif + let l:found = 0 - if l:cline == 0 && l:ccol == 0 || (l:dline < l:cline || l:dline == l:cline && l:dcol < l:ccol) - " Next comment begin after the next '.' (or no comment) so things are OK + call cursor(l:npl, l:npc) + + while(! l:found) + let [l:cline, l:ccol] = searchpos('(\*', 'cWn') + let [l:dline, l:dcol] = searchpos('\%(^\|[^.]\zs\)\.\%($\|\s\)', 'cWn') + let [l:sline, l:scol] = searchpos('"\%([^"\\]\|\\.\)*"', 'cWn') + let [l:nline, l:ncol] = s:GetLowest(l:cline, l:ccol, l:dline, l:dcol) + let [l:nline, l:ncol] = s:GetLowest(l:nline, l:ncol, l:sline, l:scol) + + call s:Debug('infonextdot', 'comment found at ' . l:cline . ', ' . l:ccol) + call s:Debug('infonextdot', 'dot found at ' . l:dline . ', ' . l:dcol) + call s:Debug('infonextdot', 'string found at ' . l:sline . ', ' . l:scol) + call s:Debug('infonextdot', 'next is ' . l:nline . ', ' . l:ncol) + + if l:nline == 0 && l:ncol == 0 + " Nothing was found. Game over. Signal EOF and out of the loop. + throw 'eof' + elseif l:nline == l:dline && l:ncol == l:dcol + " The next thing of interest is a dot. Set l:found to get out of the + " loop, and leave the mtch position in l:dline/l:dcol. let l:found = 1 - else - " Else move the cursor to the end of the comment + elseif l:nline == l:sline && l:ncol == l:scol + " Next thing is a string. Move past it and loop. + call cursor(l:sline, l:scol) + call search('"\%([^"\\]\|\\.\)*"', 'cWe') + call s:Debug('infonextdot', "end string found at " . b:curline . ', ' . b:curcol) + elseif l:nline == l:cline && l:ncol == l:ccol + " Next thing is a comment. Find its end. call cursor(l:cline, l:ccol) let [l:dline, l:dcol] = searchpairpos('(\*', '', '\*)', 'W') call s:Debug('infonextdot', '"*)" found at ' . l:dline . ', ' . l:dcol) - if l:dline == 0 && l:dcol == 0 - let l:eof = 1 + " If it didn't end, EOF + throw "eof" + else + " Move to the end, loop. + call cursor(l:dline, l:dcol) endif + else + throw "GetNextCmd: internal error" endif endwhile - if l:eof == 1 - throw 'eof' - endif - call s:Debug('infonextdot', 'Next dot is at ' . l:dline . ', ' . l:dcol) return [GetPart(b:curline, b:curcol, l:dline, l:dcol), l:dline, l:dcol, 1] From 308fe150e0b157aec115c0ee5328ac0e803cc7e7 Mon Sep 17 00:00:00 2001 From: Jonathan Sailor Date: Thu, 31 Jan 2013 18:15:15 -0500 Subject: [PATCH 3/4] Don't raise errors until the first .v file is open This means people who install the plugin in a ~/.vim/ directory they use with multiple vim versions won't get an error if one vim doesn't support perl or is missing coq if they only use .v files in the other vim. --- plugin/coq_IDE.vim | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/plugin/coq_IDE.vim b/plugin/coq_IDE.vim index 347b21b..16d7e2c 100644 --- a/plugin/coq_IDE.vim +++ b/plugin/coq_IDE.vim @@ -71,13 +71,26 @@ if exists('g:loaded_CoqIDE') endif let g:loaded_CoqIDE = 1 +function s:cant_run(why) + let s:why_cant_run = a:why + let s:has_yelled = 0 + function CoqIDE_yell_bad() + if ! s:has_yelled + echoerr s:why_cant_run + let s:has_yelled = 1 + endif + endfunction + autocmd BufEnter *.v call CoqIDE_yell_bad() + autocmd WinEnter *.v call CoqIDE_yell_bad() +endfunction + if !has('perl') - echoerr "Your vim doesn't supports perl. Install it before using CoqIde mode." + call s:cant_run("Your vim doesn't supports perl. Install it before using CoqIde mode.") finish endif if executable(s:coqtop) < 1 - echoerr s:coqtop . ': command not found.' + call s:cant_run(s:coqtop . ': command not found.') finish endif From 4999a10b15a6f76abc5e4453ab7459a3ba676b01 Mon Sep 17 00:00:00 2001 From: Jonathan Sailor Date: Thu, 31 Jan 2013 18:16:52 -0500 Subject: [PATCH 4/4] Shorten the line separating hypotheses from goals Shorten it from 70 '='s to only 38. Much more managable. --- plugin/coq_IDE.vim | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugin/coq_IDE.vim b/plugin/coq_IDE.vim index 16d7e2c..9b9d537 100644 --- a/plugin/coq_IDE.vim +++ b/plugin/coq_IDE.vim @@ -1108,14 +1108,14 @@ function s:ShowGoals(fgbg) endif call append(1, l:hyps) let l:count = 1 + len(l:hyps) - call append(l:count, '====================================================================== (1/' . l:nbgoal . ')') + call append(l:count, '============================== (1/' . l:nbgoal . ')') call append(l:count + 1, l:goal) normal kmaj let l:count += 1 + len(l:goal) let l:gnb = 2 for l:remaingoal in l:fg[1:-1] let [_, l:goal] = l:remaingoal - call append(l:count, ['', '====================================================================== (' . l:gnb . '/' . l:nbgoal . ')']) + call append(l:count, ['', '============================== (' . l:gnb . '/' . l:nbgoal . ')']) call append(l:count + 2, l:goal) let l:gnb += 1 let l:count += 2 + len(l:goal)