added shortcuts for queries

autoload/coqtop.py

@@ -1,7 +1,7 @@
 import os
 import re
 import subprocess
-import xml.etree.ElementTree as ET
+import xml.etree.cElementTree as ET
 import signal
 
 from collections import deque, namedtuple
@@ -104,7 +104,7 @@ def encode_value(v):
         xml = build('bool', str(v).lower())
         xml.text = str(v)
         return xml
-    elif isinstance(v, str):
+    elif isinstance(v, str) or isinstance(v, unicode):
         xml = build('string')
         xml.text = v
         return xml
@@ -164,7 +164,7 @@ def get_answer():
     data = ''
     while True:
         try:
-            data += os.read(fd, 0x4000)
+            data += os.read(fd, 0x10000)
             try:
                 elt = ET.fromstring('<coqtoproot>' + escape(data) + '</coqtoproot>')
                 shouldWait = True
@@ -247,7 +247,7 @@ def cur_state():
 
 def advance(cmd, encoding = 'utf-8'):
     global state_id
-    r = call('Add', ((cmd, -1), (cur_state(), True)), encoding)
+    r = call('Add', ((cmd.decode(encoding), -1), (cur_state(), True)), encoding)
     if r is None:
         return r
     if isinstance(r, Err):

autoload/coquille.vim

@@ -25,6 +25,9 @@ py if not vim.eval("s:current_dir") in sys.path:
 \    sys.path.append(vim.eval("s:current_dir")) 
 py import coquille
 
+hi Vertsplit cterm=NONE
+hi StatusLineNC cterm=NONE
+
 function! coquille#ShowPanels()
     " open the Goals & Infos panels before going back to the main window
     let l:winnb = winnr()
@@ -61,10 +64,18 @@ function! coquille#FNMapping()
     map <buffer> <silent> <F2> :CoqUndo<CR>
     map <buffer> <silent> <F3> :CoqNext<CR>
     map <buffer> <silent> <F4> :CoqToCursor<CR>
+    map <buffer> <silent> <F5> :call coquille#RawQuery("Check " . VisualSelection() . ".")<CR>
+    map <buffer> <silent> <F6> :call coquille#RawQuery("Print " . VisualSelection() . ".")<CR>
+    map <buffer> <silent> <F7> :call coquille#RawQuery("Search " . VisualSelection() . ".")<CR>
+    map <buffer> <silent> <F12> :CoqKill<CR>
 
     imap <buffer> <silent> <F2> <C-\><C-o>:CoqUndo<CR>
     imap <buffer> <silent> <F3> <C-\><C-o>:CoqNext<CR>
     imap <buffer> <silent> <F4> <C-\><C-o>:CoqToCursor<CR>
+    imap <buffer> <silent> <F5> :call coquille#RawQuery("Check " . VisualSelection() . ".")<CR>
+    imap <buffer> <silent> <F6> :call coquille#RawQuery("Print " . VisualSelection() . ".")<CR>
+    imap <buffer> <silent> <F7> :call coquille#RawQuery("Search " . VisualSelection() . ".")<CR>
+    imap <buffer> <silent> <F12> :CoqKill<CR>
 endfunction
 
 function! coquille#CoqideMapping()
@@ -124,3 +135,24 @@ function! coquille#Register()
 
     command! -bar -buffer -nargs=* -complete=file CoqLaunch call coquille#Launch(<f-args>)
 endfunction
+
+function! VisualSelection()
+    if mode()=="v"
+        let [line_start, column_start] = getpos("v")[1:2]
+        let [line_end, column_end] = getpos(".")[1:2]
+    else
+        let [line_start, column_start] = getpos("'<")[1:2]
+        let [line_end, column_end] = getpos("'>")[1:2]
+    end
+    if (line2byte(line_start)+column_start) > (line2byte(line_end)+column_end)
+        let [line_start, column_start, line_end, column_end] =
+        \   [line_end, column_end, line_start, column_start]
+    end
+    let lines = getline(line_start, line_end)
+    if len(lines) == 0
+            return ''
+    endif
+    let lines[-1] = lines[-1][: column_end - 1]
+    let lines[0] = lines[0][column_start - 1:]
+    return join(lines, "\n")
+endfunction