Add debug buffer, fix a bug

autoload/coqtop.py

@@ -24,6 +24,20 @@
 Goal = namedtuple('Goal', ['id', 'hyp', 'ccl'])
 Evar = namedtuple('Evar', ['info'])
 
+class Emptylogger:
+    def log(self, message):
+        pass
+
+logger = Emptylogger()
+
+def set_debug(l):
+    global logger
+    logger = l
+
+def info(message):
+    global logger
+    logger.log(message)
+
 def parse_response(xml):
     assert xml.tag == 'value'
     if xml.get('val') == 'good':
@@ -159,12 +173,22 @@ def escape(cmd):
               .replace("(", '(') \
               .replace(")", ')')
 
+# Extract <string> from a <message> element
+def parse_message(elt):
+    for e in elt:
+        if e.tag == 'string':
+            return parse_value(e)
+    # message without string?
+    return ''
+
 def get_answer():
     fd = coqtop.stdout.fileno()
     data = ''
+    info("RESPONSE:")
     while True:
         try:
             data += os.read(fd, 0x4000)
+            info(data)
             try:
                 elt = ET.fromstring('<coqtoproot>' + escape(data) + '</coqtoproot>')
                 shouldWait = True
@@ -176,9 +200,9 @@ def get_answer():
                         valueNode = c
                     if c.tag == 'message':
                         if messageNode is not None:
-                            messageNode = messageNode + "\n\n" + parse_value(c[2])
+                            messageNode = messageNode + "\n\n" + parse_message(c)
                         else:
-                            messageNode = parse_value(c[2])
+                            messageNode = parse_message(c)
                 if shouldWait:
                     continue
                 else:
@@ -201,6 +225,8 @@ def call(name, arg, encoding='utf-8'):
     return response
 
 def send_cmd(cmd):
+    info("SEND CMD:")
+    info(cmd)
     coqtop.stdin.write(cmd)
 
 def restart_coq(*args):

autoload/coquille.py

@@ -9,6 +9,35 @@
 import vimbufsync
 vimbufsync.check_version("0.1.0", who="coquille")
 
+class Logger:
+    def __init__(self, buf):
+        self.vim_win = None
+        for win in vim.windows:
+            if win.buffer == buf:
+                self.vim_win = win
+                break
+        if self.vim_win:
+            self.vim_win.buffer[:] = None
+            self.vim_win.buffer[0] = "START DEBUGGING"
+    def log(self, message):
+        if self.vim_win is not None:
+            for l in message.split('\n'):
+                self.vim_win.buffer.append(l)
+            self.vim_win.cursor = (len(self.vim_win.buffer), 0)
+            ori_win = vim.current.window.number
+            cmd = "execute %d . 'winc w'\n\
+                   execute %d . 'winc w'" % (self.vim_win.number, ori_win)
+            vim.command(cmd)
+
+logger = Logger(None)
+
+def set_debug(buf):
+    global logger
+    if buf:
+        logger = Logger(buf)
+    else:
+        logger = Logger(None)
+
 #: See vimbufsync ( https://github.com/def-lkb/vimbufsync )
 saved_sync = None
 
@@ -163,6 +192,8 @@ def coq_raw_query(*args):
 
 
 def launch_coq(*args):
+    global logger
+    CT.set_debug(logger)
     CT.restart_coq(*args)
 
 def debug():
@@ -198,6 +229,12 @@ def show_goal():
         print('ERROR: the Coq process died')
         return
 
+    if isinstance(response, CT.Err):
+        text = response.err.text
+        for l in text.split('\n'):
+            buff.append(l)
+        return
+
     if response.msg is not None:
         info_msg = response.msg
 

autoload/coquille.vim

@@ -38,6 +38,13 @@ function! coquille#ShowPanels()
         setlocal filetype=coq-infos
         setlocal noswapfile
         let s:info_buf = bufnr("%")
+    if exists("s:debug")
+        rightbelow new Debug
+            setlocal buftype=nofile
+            setlocal filetype=coq-debug
+            setlocal noswapfile
+            let s:debug_buf = bufnr("%")
+    endif
     execute l:winnb . 'winc w'
 endfunction
 
@@ -86,8 +93,14 @@ function! coquille#Launch(...)
     if s:coq_running == 1
         echo "Coq is already running"
     else
-        let s:coq_running = 1
+        call coquille#ShowPanels()
+        if exists("s:debug_buf")
+            py coquille.set_debug(vim.buffers[int(vim.eval("s:debug_buf"))])
+        else
+            py coquille.set_debug(None)
+        endif
 
+        let s:coq_running = 1
         " initialize the plugin (launch coqtop)
         py coquille.launch_coq(*vim.eval("map(copy(a:000),'expand(v:val)')"))
 
@@ -100,8 +113,6 @@ function! coquille#Launch(...)
 
         command! -buffer -nargs=* Coq call coquille#RawQuery(<f-args>)
 
-        call coquille#ShowPanels()
-
         " Automatically sync the buffer when entering insert mode: this is usefull
         " when we edit the portion of the buffer which has already been sent to coq,
         " we can then rewind to the appropriate point.
@@ -113,6 +124,10 @@ function! coquille#Launch(...)
     endif
 endfunction
 
+function! coquille#DebugOn()
+    let s:debug = 1
+endfunction
+
 function! coquille#Register()
     hi default CheckedByCoq ctermbg=17 guibg=LightGreen
     hi default SentToCoq ctermbg=60 guibg=LimeGreen