From efc4fe55454948872b65ef4dfa13fb54ec2da00b Mon Sep 17 00:00:00 2001 From: Wang Nan Date: Sat, 16 Dec 2017 02:04:05 +0800 Subject: [PATCH 1/3] Add debug buffer for debugging Usage: :call coquille#DebugOn() :CoqLaunch Will open a new buffer named "Debug". Message to/from coqtop will be shown there. Signed-off-by: Wang Nan --- autoload/coqtop.py | 18 ++++++++++++++++++ autoload/coquille.py | 31 +++++++++++++++++++++++++++++++ autoload/coquille.vim | 21 ++++++++++++++++++--- 3 files changed, 67 insertions(+), 3 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 8d35600..ef30396 100644 --- a/autoload/coqtop.py +++ b/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': @@ -162,9 +176,11 @@ def escape(cmd): def get_answer(): fd = coqtop.stdout.fileno() data = '' + info("RESPONSE:") while True: try: data += os.read(fd, 0x4000) + info(data) try: elt = ET.fromstring('' + escape(data) + '') shouldWait = True @@ -201,6 +217,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): diff --git a/autoload/coquille.py b/autoload/coquille.py index 67e54f3..2972ea9 100644 --- a/autoload/coquille.py +++ b/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(): diff --git a/autoload/coquille.vim b/autoload/coquille.vim index 0e5045f..2a9429d 100644 --- a/autoload/coquille.vim +++ b/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() - 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 From 6d5ef3d76cc91f3dca0ff7797b6c5b6c324119fb Mon Sep 17 00:00:00 2001 From: Wang Nan Date: Sun, 17 Dec 2017 23:17:38 +0800 Subject: [PATCH 2/3] Parse node correctly Message can be reported this way: mypred_Sx is defined When recving message like this, python raise an exception in get_answer() because accessing 'c[2]' is invalid in this case. We should look for the exact node instead. Signed-off-by: Wang Nan --- autoload/coqtop.py | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index ef30396..6997bed 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -173,6 +173,14 @@ def escape(cmd): .replace("(", '(') \ .replace(")", ')') +# Extract from a 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 = '' @@ -192,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: From ad9e131756efe65ccaa9994d0e7463fa02ec53c9 Mon Sep 17 00:00:00 2001 From: Wang Nan Date: Thu, 21 Dec 2017 23:38:12 +0800 Subject: [PATCH 3/3] Display error message correctly When coqtop response an error, try to extract 'msg' field from response, cause an exception. Before parsing goals, check if response is Err. Signed-off-by: Wang Nan --- autoload/coquille.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/autoload/coquille.py b/autoload/coquille.py index 2972ea9..f67165c 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -229,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