From 6719ee5b093ff4c5bd72d38e2da10bd7ffdb4721 Mon Sep 17 00:00:00 2001 From: lucas8 Date: Sun, 9 Apr 2017 00:48:16 +0200 Subject: [PATCH 01/12] improve coq error handling Python no longer fails for most of coq errors. When sending an invalid argument during a proof, an error is displayed in the info box, but the cursor moves over the instruction : it may not be intuitive. Furthermote, moving to a Qed like that creates another python error. --- autoload/coqtop.py | 17 +++++++++++++---- autoload/coquille.py | 22 ++++++++++++---------- 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 8d35600..2d2a946 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -7,7 +7,7 @@ from collections import deque, namedtuple Ok = namedtuple('Ok', ['val', 'msg']) -Err = namedtuple('Err', ['err']) +Err = namedtuple('Err', ['err', 'loc_s', 'loc_e']) Inl = namedtuple('Inl', ['val']) Inr = namedtuple('Inr', ['val']) @@ -29,8 +29,9 @@ def parse_response(xml): if xml.get('val') == 'good': return Ok(parse_value(xml[0]), None) elif xml.get('val') == 'fail': - print('err: %s' % ET.tostring(xml)) - return Err(parse_error(xml)) + # Don't print the error immediately : let the caller decide wether + # it must be printed and in which way + return parse_error(xml) else: assert False, 'expected "good" or "fail" in ' @@ -86,7 +87,9 @@ def parse_value(xml): return ''.join(xml.itertext()) def parse_error(xml): - return ET.fromstring(re.sub(r"", '', ET.tostring(xml))) + loc_s = xml.get('loc_s') + loc_e = xml.get('loc_e') + return Err('Err: ' + loc_s + ' to ' + loc_e, int(loc_s), int(loc_e)) def build(tag, val=None, children=()): attribs = {'val': val} if val is not None else {} @@ -179,6 +182,9 @@ def get_answer(): messageNode = messageNode + "\n\n" + parse_value(c[2]) else: messageNode = parse_value(c[2]) + # Extract messages from feedbacks to handle errors + if c.tag == 'feedback' and c[1].get('val') == 'message': + messageNode = parse_value(c[1][0][2]) if shouldWait: continue else: @@ -186,6 +192,9 @@ def get_answer(): if messageNode is not None: if isinstance(vp, Ok): return Ok(vp.val, messageNode) + elif isinstance(vp, Err): + # Override error message : coq provides one + return Err(messageNode, vp.loc_s, vp.loc_e) return vp except ET.ParseError: continue diff --git a/autoload/coquille.py b/autoload/coquille.py index 67e54f3..dfc04b0 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -78,7 +78,7 @@ def coq_rewind(steps=1): if isinstance(response, CT.Ok): encountered_dots = encountered_dots[:len(encountered_dots) - steps] else: - info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response + info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response.err refresh() @@ -154,8 +154,7 @@ def coq_raw_query(*args): if response.msg is not None: info_msg = response.msg elif isinstance(response, CT.Err): - info_msg = response.err.text - print("FAIL") + info_msg = response.err else: print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) # ugly @@ -198,8 +197,13 @@ def show_goal(): print('ERROR: the Coq process died') return - if response.msg is not None: - info_msg = response.msg + if isinstance(response, CT.Ok): + if response.msg is not None: + info_msg = response.msg + elif isinstance(response, CT.Err): + if response.err is not None: + info_msg = response.err + return if response.val.val is None: buff.append('No goals.') @@ -335,12 +339,10 @@ def send_until_fail(): else: send_queue.clear() if isinstance(response, CT.Err): - response = response.err - info_msg = response.text - loc_s = response.get('loc_s') + info_msg = response.err + loc_s = response.loc_s if loc_s is not None: - loc_s = int(loc_s) - loc_e = int(response.get('loc_e')) + loc_e = response.loc_e (l, c) = message_range['start'] (l_start, c_start) = _pos_from_offset(c, message, loc_s) (l_stop, c_stop) = _pos_from_offset(c, message, loc_e) From b2288de20a39f6a78899ddd2122cd058c0145b7e Mon Sep 17 00:00:00 2001 From: lucas8 Date: Sun, 9 Apr 2017 01:01:17 +0200 Subject: [PATCH 02/12] no more python errors on Qed with subgoals --- autoload/coqtop.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 2d2a946..2194bb4 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -87,9 +87,13 @@ def parse_value(xml): return ''.join(xml.itertext()) def parse_error(xml): + print(xml) loc_s = xml.get('loc_s') loc_e = xml.get('loc_e') - return Err('Err: ' + loc_s + ' to ' + loc_e, int(loc_s), int(loc_e)) + if loc_s is not None: + return Err('Err: ' + loc_s + ' to ' + loc_e, int(loc_s), int(loc_e)) + else: + return Err('Err: invalid', None, None) def build(tag, val=None, children=()): attribs = {'val': val} if val is not None else {} From ec0d19f10610084c2e2bb18b4cd5e1a88b9bcd38 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sun, 20 Aug 2017 13:40:15 -0700 Subject: [PATCH 03/12] Allow multiple coq buffers to opened at the same time 1. Allow multiple instances of coqtop to run for different coq source buffers. 2. Support python 2 or 3. 3. Parse default coqtop args from _CoqProject 4. Allow multiple line ranges for the checked, sent, and error regions. This shows when coq processes statements out of order. 5. Fix parsing comments longer than 995 lines 6. Fix parsing strings over 995 lines 7. Add a utility to capture protocol traces from coqide 8. Use better default colors when the background is dark --- README.md | 71 ++- autoload/coqtop-log.py | 87 +++ autoload/coqtop.py | 446 +++++++++++----- autoload/coquille.py | 1093 ++++++++++++++++++++------------------ autoload/coquille.vim | 846 +++++++++++++++++++++++++++-- autoload/project_file.py | 98 ++++ ftdetect/coq.vim | 4 +- 7 files changed, 1939 insertions(+), 706 deletions(-) create mode 100755 autoload/coqtop-log.py create mode 100644 autoload/project_file.py diff --git a/README.md b/README.md index 6e7924b..19a83ee 100644 --- a/README.md +++ b/README.md @@ -32,16 +32,14 @@ branch. Getting started --------------- -To launch Coquille on your Coq file, run `:CoqLaunch` which will make the -commands : - +When a coq type file is loaded (anything with a .v extension), these commands become available: +- CoqLaunch {coqtop arg} .. +- Coq {vernacular command} .. - CoqNext - CoqToCursor - CoqUndo - CoqKill -available to you. - By default Coquille forces no mapping for these commands, however two sets of mapping are already defined and you can activate them by adding : @@ -55,7 +53,35 @@ or to your `.vimrc`. -Alternatively you can, of course, define your owns. +Alternatively you can, of course, define your own. + +Starting Coq +------------ + +Coquille will implicitly start coqtop when any of its commands are run. +Coquille will parse the \_CoqProject for options to pass to coqtop. This +behavior can be disabled by setting `g:coquille_append_project_args` to 0. + +Additional arguments for coqtop can be specified by explicitly starting coqtop +using `:CoqLaunch`. + +Multiple files +-------------- + +Coquille supports having multiple coq source files (.v files) open at the same +time. The coq source files can be in separate tabs, different windows (splits) +within the same tab, or switching between hidden buffers in the same window. + +When coquille is first started in a tab, it will create an info panel and a +goals panel (split). By default if more source windows are added to the same +tab, coquille will reuse the existing info and goals panels for the new source +windows. Whenever the active source window is switched, the corresponding info +and goals buffers will be displayed in their panels -- hiding the previous +info and goals buffers. + +Alternatively `g:coquilled_shared` can be set to 0, which tells coquille to +create separate info and goals panels for each coq source window. It can also +be changed on a per window basis by setting `w:coquille_shared`. Running query commands ---------------------- @@ -69,8 +95,9 @@ Configuration Note that the color of the "lock zone" is hard coded and might not be pretty in your specific setup (depending on your terminal, colorscheme, etc). -To change it, you can overwrite the `CheckedByCoq` and `SentToCoq` highlight -groups (`:h hi` and `:h highlight-groups`) to colors that works better for you. +To change it, you can overwrite the `CheckedByCoq`, `SentToCoq`, `CoqError`, +and `CoqWarning` highlight groups (`:h hi` and `:h highlight-groups`) to colors +that works better for you. See [coquille.vim][5] for an example. You can set the following variable to modify Coquille's behavior: @@ -79,7 +106,31 @@ You can set the following variable to modify Coquille's behavior: (default = 'false') move your cursor to the end of the lock zone after calls to CoqNext or CoqUndo -Screenshoots + g:coquille_shared Set it to 0 to cause Coquille to create new + (default = 1) info and goals panels for each source + window in a tab. + + g:coquille_append_project_args When set to non-zero, \_CoqProject is parsed + (default = 1) for args to pass to coqtop. + + g:coquille_keep_open Set it to 1 to prevent Coquille from + (default = 0) closing the info and goals panels when they + are no longer referenced by any coq source + windows. This is useful to prevent the + window layout from changing when a non-coq + source file is edited in the coq source + window and the coq source file is not + hidden. + +Python version +-------------- + +Coquille requires python 2 or python 3 support in vim. If both are available, +Coquille will use python 3. Once Coquille uses python 3, that prevents the vim +from using python 2 in any other plugins. You can force Coquille to use python +2 by putting `:call has('python')` in your `.vimrc`. + +Screenshots ------------ Because pictures are always the best sellers : @@ -90,4 +141,4 @@ Because pictures are always the best sellers : [2]: https://github.com/def-lkb/vimbufsync [3]: http://www.vim.org/scripts/script.php?script_id=2063 "coq syntax on vim.org" [4]: http://www.vim.org/scripts/script.php?script_id=2079 "coq indent on vim.org" -[5]: https://github.com/the-lambda-church/coquille/blob/master/autoload/coquille.vim#L103 +[5]: https://github.com/the-lambda-church/coquille/blob/master/autoload/coquille.vim#L813 diff --git a/autoload/coqtop-log.py b/autoload/coqtop-log.py new file mode 100755 index 0000000..7e1244f --- /dev/null +++ b/autoload/coqtop-log.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python + +# To use this, rename coqtop into coqtop.real, then put this script in its +# place. This script will save all xml communication with coqtop in a log file. + +from __future__ import print_function + +import os +import subprocess +import sys +import threading +import xml.parsers.expat + +xml_io = "-ideslave" in sys.argv + +log = open("coq-xml-log-%d.txt" % os.getpid(), "w") +print("Running %s" % sys.argv, file=log) +log.flush() + +# Fake the HTML entities. This does not link to the real html DTD so that expat +# does not try to download the real DTD. +coq_doc_type = """ +]>""" + +def get_doc_end(xml_buffer): + if not xml_io: + if len(xml_buffer): + return len(xml_buffer) + else: + return -1 + parser = xml.parsers.expat.ParserCreate() + try: + parser.Parse(coq_doc_type + xml_buffer, True) + end = len(xml_buffer) + except xml.parsers.expat.ExpatError as e: + if e.message.startswith(xml.parsers.expat.errors.XML_ERROR_JUNK_AFTER_DOC_ELEMENT): + end = parser.ErrorByteIndex - len(coq_doc_type) + else: + end = -1 + return end + +def handle_input(name, from_fd, to_file): + xml_buffer = "" + while True: + read = os.read(from_fd, 10000) + if read == "": + break + xml_buffer += read + while True: + try: + end = get_doc_end(xml_buffer) + except xml.parsers.expat.ExpatError as e: + print("%s: Error parsing %s: %s" % (name, xml_buffer, e), + file=log) + log.flush() + raise + if end != -1: + print("%s: %s" % (name, xml_buffer[0:end]), file=log) + log.flush() + to_file.write(xml_buffer[0:end]) + to_file.flush() + xml_buffer = xml_buffer[end:] + else: + break + to_file.close() + +real_coq = subprocess.Popen(args=([sys.argv[0] + ".real"] + sys.argv[1:]), + stdin=subprocess.PIPE, + stdout=subprocess.PIPE) + +input_thread = threading.Thread(target=handle_input, + args=("input", sys.stdin.fileno(), real_coq.stdin)) +output_thread = threading.Thread(target=handle_input, + args=("output", real_coq.stdout.fileno(), sys.stdout)) +# There is no good way to stop the input thread if real_coq exits early. So +# start it as a daemon thread and let it get force aborted at the end. +input_thread.daemon = True +input_thread.start() +output_thread.start() + +real_coq.wait() + +os.close(sys.stdin.fileno()) +output_thread.join() + +sys.exit(real_coq.returncode) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 2194bb4..fedc818 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -1,17 +1,26 @@ +from __future__ import print_function +from __future__ import unicode_literals +from __future__ import division + import os import re import subprocess import xml.etree.ElementTree as ET import signal +import sys from collections import deque, namedtuple +# Define unicode in python 3 +unicode = getattr(__builtins__, 'unicode', str) + Ok = namedtuple('Ok', ['val', 'msg']) -Err = namedtuple('Err', ['err', 'loc_s', 'loc_e']) +Err = namedtuple('Err', ['err', 'revert_state', 'loc_s', 'loc_e']) Inl = namedtuple('Inl', ['val']) Inr = namedtuple('Inr', ['val']) +EditId = namedtuple('EditId', ['id']) StateId = namedtuple('StateId', ['id']) Option = namedtuple('Option', ['val']) @@ -49,6 +58,8 @@ def parse_value(xml): return xml.text or '' elif xml.tag == 'int': return int(xml.text) + elif xml.tag == 'edit_id': + return EditId(int(xml.get('val'))) elif xml.tag == 'state_id': return StateId(int(xml.get('val'))) elif xml.tag == 'list': @@ -87,13 +98,20 @@ def parse_value(xml): return ''.join(xml.itertext()) def parse_error(xml): - print(xml) loc_s = xml.get('loc_s') loc_e = xml.get('loc_e') + msg = xml.find("richpp") + if msg is not None: + msg = parse_value(msg).strip() + else: + msg = "Err: unknown" + revert_state = xml.find("state_id") + if revert_state is not None: + revert_state = parse_value(revert_state) if loc_s is not None: - return Err('Err: ' + loc_s + ' to ' + loc_e, int(loc_s), int(loc_e)) + return Err(msg, revert_state, int(loc_s), int(loc_e)) else: - return Err('Err: invalid', None, None) + return Err(msg, revert_state, None, None) def build(tag, val=None, children=()): attribs = {'val': val} if val is not None else {} @@ -111,7 +129,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 @@ -119,6 +137,8 @@ def encode_value(v): xml = build('int') xml.text = str(v) return xml + elif isinstance(v, EditId): + return build('edit_id', str(v.id)) elif isinstance(v, StateId): return build('state_id', str(v.id)) elif isinstance(v, list): @@ -142,21 +162,6 @@ def encode_value(v): else: assert False, 'unrecognized type in encode_value: %r' % (type(v),) -coqtop = None -states = [] -state_id = None -root_state = None - -def kill_coqtop(): - global coqtop - if coqtop: - try: - coqtop.terminate() - coqtop.communicate() - except OSError: - pass - coqtop = None - def ignore_sigint(): signal.signal(signal.SIGINT, signal.SIG_IGN) @@ -166,123 +171,306 @@ def escape(cmd): .replace("(", '(') \ .replace(")", ')') -def get_answer(): - fd = coqtop.stdout.fileno() - data = '' - while True: - try: - data += os.read(fd, 0x4000) +class Command(object): + # Command was sent to coqtop through an Add call, and coq acknowledged the + # Add. + SENT = 0 + # The worker that was processing this command died before finishing + # processing the command. The command will never be finished. + ABANDONED = 1 + # coqtop marked the command as processed through a feedback statement. + PROCESSED = 2 + # coqtop sent a warning level message for the command through a feedback + # statement. + WARNING = 3 + # coqtop sent an error level message for the command through a feedback + # statement. + ERROR = 4 + + next_edit = -1 + + def __init__(self, end): + self.edit_id = EditId(Command.next_edit) + Command.next_edit -= 1 + self.state_id = None + self.state = self.SENT + # A (line, col) pair. Both the line and col are 0-indexed. The end + # position is one column after the last character included in the + # command. + self.end = end + # A byte offset relative to the start of this command where the warning + # or error starts. + self.msg_start_offset = None + # A (line, col) pair where the warning/error state starts + self.msg_start = None + # A byte offset relative to the start of this command where the warning + # or error stops. + self.msg_stop_offset = None + # A (line, col) pair where the warning/error state stops + self.msg_stop = None + # The worker that was last processing this command + self.worker = None + +class CoqTop(object): + def __init__(self): + self.coqtop = None + self.states = [] + # A list of states that were reverted. These stick around until the + # error messages are cleared, to track where the errors are in the + # reverted commands. This is important because sometimes coqtop forces + # the state to get reverted. + # the states to get reverted. + self.reverted_states = [] + self.error_messages = [] + + def kill_coqtop(self): + if self.coqtop: try: - elt = ET.fromstring('' + escape(data) + '') - shouldWait = True - valueNode = None - messageNode = None - for c in elt: - if c.tag == 'value': - shouldWait = False - valueNode = c - if c.tag == 'message': - if messageNode is not None: - messageNode = messageNode + "\n\n" + parse_value(c[2]) - else: - messageNode = parse_value(c[2]) - # Extract messages from feedbacks to handle errors - if c.tag == 'feedback' and c[1].get('val') == 'message': - messageNode = parse_value(c[1][0][2]) - if shouldWait: - continue - else: + self.coqtop.terminate() + self.coqtop.communicate() + except OSError: + pass + self.coqtop = None + self.states = [] + self.clear_errors() + + def get_command(self, state_id): + for s in self.states: + if s.state_id == state_id: + return s + return None + + def get_command_by_edit(self, edit_id): + for s in self.states: + if s.edit_id == edit_id: + return s + return None + + def parse_feedback(self, xml): + assert xml.tag == 'feedback' + message = None + if xml.get("object") == "state": + state_id = parse_value(xml.find("state_id")) + comm = self.get_command(state_id) + else: + edit_id = parse_value(xml.find("edit_id")) + comm = self.get_command_by_edit(edit_id) + feedback_content = xml.find("feedback_content") + feedback_type = feedback_content.get('val') + if feedback_type == "message": + messageNode = feedback_content.find("message") + level = messageNode.find("message_level") + level = level.get("val") + if level == "error": + level = Command.ERROR + else: + level = Command.WARNING + if comm: + comm.state = level + # The element type is option + if messageNode[1].get("val") == "some": + loc = messageNode[1].find("loc") + comm.msg_start_offset = int(loc.get("start")) + comm.msg_stop_offset = int(loc.get("stop")) + message = parse_value(messageNode.find("richpp")) + self.error_messages.append(message) + elif feedback_type == "processingin": + if comm is not None: + comm.worker = parse_value(feedback_content[0]) + elif feedback_type == "workerstatus": + (worker, status) = parse_value(feedback_content[0]) + if status == "Dead": + # The worker died. Mark all commands it was processing as + # abandoned. + for c in self.states: + if c.state == Command.SENT and c.worker == worker: + c.state = Command.ABANDONED + elif feedback_type == "processed": + # Only transition from SENT to PROCESSED. coqtop likes to send out + # extra feedback messages. Do not let it transition the command + # from WARNING to PROCESSED. + # + # Also note that sometimes coqtop sends processed feedback for + # commands that it hasn't sent the Add reply for yet. Its difficult + # to process the feedback when the correspondance between the + # Command and state_id isn't known yet. So that feedback can be + # ignored. coqtop will send another processed feedback after the + # Add reply is sent. + if comm and comm.state == Command.SENT: + comm.state = Command.PROCESSED + return message + + def parse_message(self, xml): + assert xml.tag == 'message' + level = xml.find('message_level') + if level is not None: + level = level.get('val') + if level == 'warning' and self.states: + comm = self.states[-1] + if comm.state_id is None: + # Attach the warning message to the command that is currently being + # parsed. + comm.state = Command.WARNING + self.error_messages.append(parse_value(xml[2])) + + def process_response(self): + fd = self.coqtop.stdout.fileno() + data = '' + while True: + try: + data += os.read(fd, 0x4000).decode("utf-8") + try: + elt = ET.fromstring('' + escape(data) + '') + # The data parsed correctly. Clear it so that it isn't + # parsed again when new data comes in. + data = '' + valueNode = None + messageNode = None + for c in elt: + if c.tag == 'value': + valueNode = c + if c.tag == 'message': + self.parse_message(c) + # Extract messages from feedbacks to handle errors + if c.tag == 'feedback': + messageNode = self.parse_feedback(c) + if valueNode is None: + return None vp = parse_response(valueNode) if messageNode is not None: if isinstance(vp, Ok): return Ok(vp.val, messageNode) elif isinstance(vp, Err): + if vp.err not in self.error_messages: + self.error_messages.append(vp.err) # Override error message : coq provides one - return Err(messageNode, vp.loc_s, vp.loc_e) + return Err(messageNode, vp.revert_state, + vp.loc_s, vp.loc_e) return vp - except ET.ParseError: - continue - except OSError: - # coqtop died - return None - -def call(name, arg, encoding='utf-8'): - xml = encode_call(name, arg) - msg = ET.tostring(xml, encoding) - send_cmd(msg) - response = get_answer() - return response - -def send_cmd(cmd): - coqtop.stdin.write(cmd) - -def restart_coq(*args): - global coqtop, root_state, state_id - if coqtop: kill_coqtop() - options = [ 'coqtop' - , '-ideslave' - , '-main-channel' - , 'stdfds' - , '-async-proofs' - , 'on' - ] - try: - if os.name == 'nt': - coqtop = subprocess.Popen( - options + list(args) - , stdin = subprocess.PIPE - , stdout = subprocess.PIPE - , stderr = subprocess.STDOUT - ) - else: - coqtop = subprocess.Popen( - options + list(args) - , stdin = subprocess.PIPE - , stdout = subprocess.PIPE - , preexec_fn = ignore_sigint - ) - - r = call('Init', Option(None)) - assert isinstance(r, Ok) - root_state = r.val - state_id = r.val - except OSError: - print("Error: couldn't launch coqtop") - -def launch_coq(*args): - restart_coq(*args) - -def cur_state(): - if len(states) == 0: - return root_state - else: - return state_id + except ET.ParseError: + continue + except OSError: + # coqtop died + return Err("coq died", 0, None, None) + + def get_answer(self, feedback_callback): + answer = None + while True: + answer = self.process_response() + if answer is not None: + return answer + # The only way None could have been returned is if feedback was + # processed instead. + if feedback_callback is not None: + feedback_callback() + + def call(self, name, arg, encoding='utf-8', feedback_callback=None): + xml = encode_call(name, arg) + msg = ET.tostring(xml, encoding) + self.send_cmd(msg) + response = self.get_answer(feedback_callback) + return response + + def send_cmd(self, cmd): + self.coqtop.stdin.write(cmd) + self.coqtop.stdin.flush() + + def restart_coq(self, *args): + if self.coqtop: self.kill_coqtop() + options = [ 'coqtop' + , '-ideslave' + , '-main-channel' + , 'stdfds' + , '-async-proofs' + , 'on' + ] + try: + if os.name == 'nt': + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , stderr = subprocess.STDOUT + ) + else: + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , preexec_fn = ignore_sigint + ) + + r = self.call('Init', Option(None)) + assert isinstance(r, Ok) + comm = Command((0, 0)) + comm.edit_id = None + comm.state_id = r.val + comm.state = Command.PROCESSED + self.states = [comm] + return True + except OSError as e: + print("Error: couldn't launch coqtop:", e) + return False -def advance(cmd, encoding = 'utf-8'): - global state_id - r = call('Add', ((cmd, -1), (cur_state(), True)), encoding) - if r is None: + def launch_coq(self, *args): + return self.restart_coq(*args) + + def cur_state(self): + return self.states[-1].state_id + + # Clear the error messages from old commands. + # + # The error state and location of non-reverted commands will stay, but + # their error messages will be reverted. + def clear_errors(self): + self.reverted_states = [] + self.error_messages = [] + + def get_errors(self): + return "\n".join(self.error_messages) + + def advance(self, cmd, end, encoding = 'utf-8'): + cur_state = self.cur_state() + comm = Command(end) + self.states.append(comm) + r = self.call('Add', ((cmd, comm.edit_id.id), + (cur_state, True)), encoding) + if r is None or isinstance(r, Err): + self.states = self.states[:len(self.states)-1] + self.reverted_states = [comm] + self.reverted_states + return r + comm.state_id = r.val[0] return r - if isinstance(r, Err): + + def rewind(self, step = 1, keep_states = False): + assert step <= len(self.states) + # At least one state, the root state, has to remain + assert step < len(self.states) + idx = len(self.states) - step + if keep_states: + self.reverted_states = self.states[idx:] + self.reverted_states + self.states = self.states[0:idx] + return self.call('Edit_at', self.cur_state()) + + def query(self, cmd, encoding = 'utf-8'): + r = self.call('Query', (cmd, self.cur_state()), encoding) return r - states.append(state_id) - state_id = r.val[0] - return r - -def rewind(step = 1): - global states, state_id - assert step <= len(states) - idx = len(states) - step - state_id = states[idx] - states = states[0:idx] - return call('Edit_at', state_id) - -def query(cmd, encoding = 'utf-8'): - r = call('Query', (cmd, cur_state()), encoding) - return r - -def goals(): - return call('Goal', ()) - -def read_states(): - return states + + def has_unchecked_commands(self): + return any(c.state == Command.SENT for c in self.states) + + def goals(self, feedback_callback): + vp = self.call('Goal', (), feedback_callback=feedback_callback) + if isinstance(vp, Ok): + return vp + # An error occurred. Revert back to the state coqtop requested, and ask + # for the goal again. + revert_count = 0 + while (revert_count < len(self.states) and + self.states[-1 - revert_count].state_id.id > vp.revert_state.id): + revert_count += 1 + self.rewind(revert_count, keep_states = True) + return self.call('Goal', (), feedback_callback=feedback_callback) + + def read_states(self): + return self.states diff --git a/autoload/coquille.py b/autoload/coquille.py index dfc04b0..8cd4fc6 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -1,357 +1,636 @@ +from __future__ import print_function +from __future__ import unicode_literals +from __future__ import division + import vim +import itertools import re import xml.etree.ElementTree as ET import coqtop as CT +import project_file from collections import deque import vimbufsync -vimbufsync.check_version("0.1.0", who="coquille") - -#: See vimbufsync ( https://github.com/def-lkb/vimbufsync ) -saved_sync = None - -#: Keeps track of what have been checked by Coq, and what is waiting to be -#: checked. -encountered_dots = [] -send_queue = deque([]) - -error_at = None +vimbufsync.check_version([0,1,0], who="coquille") -info_msg = None +# Define unicode in python 3 +unicode = getattr(__builtins__, 'unicode', str) -################### -# synchronization # -################### +# Cache whether vim has a bool type +vim_has_bool = vim.eval("exists('v:false')") -def sync(): - global saved_sync - curr_sync = vimbufsync.sync() - if not saved_sync or curr_sync.buf() != saved_sync.buf(): - _reset() - else: - (line, col) = saved_sync.pos() - rewind_to(line - 1, col) # vim indexes from lines 1, coquille from 0 - saved_sync = curr_sync +def vim_repr(value): + "Converts a python value into a vim value" + if isinstance(value, bool): + if value: + if vim_has_bool: + return "v:true" + else: + return "1" + else: + if vim_has_bool: + return "v:false" + else: + return "0" + if isinstance(value, int) or isinstance(value, long): + return str(value) + if isinstance(value, bytes): + value = value.decode("utf-8") + if isinstance(value, unicode): + return value.replace("'", "''") + return "unknown" + +# Convert 0-based (line, col) pairs into 1-based lists +def make_vim_range(start, stop): + return [[start[0] + 1, start[1] + 1], [stop[0] + 1, stop[1] + 1]] + +# All the python side state associated with the vim source buffer +class BufferState(object): + # Dict mapping source buffer id to BufferState + source_mapping = {} + + @classmethod + def lookup_bufid(cls, bufid): + # For convenience, the vim script passes vim.eval("l:bufid") to this + # function, and vim.eval() returns a string. + bufid = int(bufid) + if bufid in cls.source_mapping: + state = cls.source_mapping[bufid] + else: + state = BufferState(vim.buffers[bufid]) + cls.source_mapping[bufid] = state + if state.sync_vars(): + return state + else: + del cls.source_mapping[bufid] + return None + + def __init__(self, source_buffer): + self.source_buffer = source_buffer + self.info_buffer = None + self.goal_buffer = None + #: See vimbufsync ( https://github.com/def-lkb/vimbufsync ) + self.saved_sync = None + + #: Keeps track of what have been checked by Coq, and what is waiting to be + #: checked. + self.send_queue = deque([]) + + self.error_at = None + + self.coq_top = CT.CoqTop() + + def sync_vars(self): + "Updates python member variables based on the vim variables" + if not self.source_buffer.valid: + return False + if self.source_buffer.options["filetype"] != b"coq": + return False + goal_bufid = self.source_buffer.vars.get("coquille_goal_bufid", -1) + if goal_bufid != -1: + self.goal_buffer = vim.buffers[goal_bufid] + else: + self.goal_buffer = None + info_bufid = self.source_buffer.vars.get("coquille_info_bufid", -1) + if info_bufid != -1: + self.info_buffer = vim.buffers[info_bufid] + else: + self.info_buffer = None + return True -def _reset(): - global saved_sync, encountered_dots, info_msg, error_at, send_queue - encountered_dots = [] - send_queue = deque([]) - saved_sync = None - error_at = None - info_msg = None - reset_color() + ################### + # synchronization # + ################### -##################### -# exported commands # -##################### + def sync(self): + curr_sync = vimbufsync.sync(self.source_buffer) + if not self.saved_sync or curr_sync.buf() != self.saved_sync.buf(): + if len(self.coq_top.states) > 1: + self._reset() + else: + (line, col) = self.saved_sync.pos() + self.rewind_to(line - 1, col) # vim indexes from lines 1, coquille from 0 + self.saved_sync = curr_sync + + def _reset(self): + self.coq_top.kill_coqtop() + self.send_queue = deque([]) + self.saved_sync = None + self.error_at = None + self.reset_color() + + ##################### + # exported commands # + ##################### + + def kill_coqtop(self): + if self is None: + return + self._reset() -def kill_coqtop(): - CT.kill_coqtop() - _reset() + def goto_last_sent_dot(self): + (line, col) = ((0,1) if not self.coq_top.states + else self.coq_top.states[-1].end) + vim.current.window.cursor = (line + 1, col) -def goto_last_sent_dot(): - (line, col) = (0,1) if encountered_dots == [] else encountered_dots[-1] - vim.current.window.cursor = (line + 1, col) + def coq_rewind(self, steps=1): + self.clear_info() -def coq_rewind(steps=1): - clear_info() + # Do not allow the root state to be rewound + if steps < 1 or len(self.coq_top.states) < 2: + return - global encountered_dots, info_msg + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - if steps < 1 or encountered_dots == []: - return + response = self.coq_top.rewind(steps) - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - response = CT.rewind(steps) + self.refresh() - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return + # steps != 1 means that either the user called "CoqToCursor" or just started + # editing in the "locked" zone. In both these cases we don't want to move + # the cursor. + if (steps == 1 and vim.eval('g:coquille_auto_move') == 'true'): + self.goto_last_sent_dot() - if isinstance(response, CT.Ok): - encountered_dots = encountered_dots[:len(encountered_dots) - steps] - else: - info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response.err + def coq_to_cursor(self): + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - refresh() + self.sync() - # steps != 1 means that either the user called "CoqToCursor" or just started - # editing in the "locked" zone. In both these cases we don't want to move - # the cursor. - if (steps == 1 and vim.eval('g:coquille_auto_move') == 'true'): - goto_last_sent_dot() + (cline, ccol) = vim.current.window.cursor + (line, col) = ((0,0) if not self.coq_top.states + else self.coq_top.states[-1].end) -def coq_to_cursor(): - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + if cline < line or (cline == line and ccol < col): + self.rewind_to(cline - 1, ccol) + else: + while True: + r = self._get_message_range((line, col)) + if r is not None and r['stop'] <= (cline - 1, ccol): + line = r['stop'][0] + col = r['stop'][1] + 1 + self.send_queue.append(r) + else: + break + + self.send_until_fail() + + def coq_next(self): + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - sync() + self.sync() - (cline, ccol) = vim.current.window.cursor - (line, col) = encountered_dots[-1] if encountered_dots else (0,0) + (line, col) = ((0,0) if not self.coq_top.states + else self.coq_top.states[-1].end) + message_range = self._get_message_range((line, col)) - if cline < line or (cline == line and ccol < col): - rewind_to(cline - 1, ccol) - else: - while True: - r = _get_message_range((line, col)) - if r is not None and r['stop'] <= (cline - 1, ccol): - line = r['stop'][0] - col = r['stop'][1] + 1 - send_queue.append(r) - else: - break + if message_range is None: return - send_until_fail() + self.send_queue.append(message_range) -def coq_next(): - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + self.send_until_fail() - sync() + if (vim.eval('g:coquille_auto_move') == 'true'): + self.goto_last_sent_dot() - (line, col) = encountered_dots[-1] if encountered_dots else (0,0) - message_range = _get_message_range((line, col)) + def coq_raw_query(self, *args): + self.clear_info() - if message_range is None: return + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - send_queue.append(message_range) + raw_query = ' '.join(args) - send_until_fail() + encoding = vim.eval("&encoding") or 'utf-8' - if (vim.eval('g:coquille_auto_move') == 'true'): - goto_last_sent_dot() + response = self.coq_top.query(raw_query, encoding) -def coq_raw_query(*args): - clear_info() + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - global info_msg - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + info_msg = self.coq_top.get_errors() + self.show_info(info_msg) + + + def launch_coq(self, *args): + use_project_args = self.source_buffer.vars.get( + "coquille_append_project_args", + vim.vars.get("coquille_append_project_args", 0)) + if use_project_args: + # Vim passes the args as a tuple + args = list(args) + args.extend(project_file.find_and_parse_file( + self.source_buffer.name)) + return self.coq_top.restart_coq(*args) + + def debug(self): + if self.coq_top.states: + print("encountered dots = [") + for (line, col) in self.coq_top.states: + print(" (%d, %d) ; " % (line, col)) + print("]") + + ##################################### + # IDE tools: Goal, Infos and colors # + ##################################### + + def refresh(self): + last_info = None + def update(): + nonlocal last_info + self.reset_color() + vim.command('redraw') + new_info = self.coq_top.get_errors() + if last_info != new_info: + self.show_info(new_info) + last_info = new_info + # It seems that coqtop needs some kind of call like Status or Goal to + # trigger it to start processing all the commands that have been added. + # So show_goal needs to be called before waiting for all the unchecked + # commands finished. + self.show_goal(update) + while self.coq_top.has_unchecked_commands(): + self.coq_top.process_response() + update() + update() + + def show_goal(self, feedback_callback): + # Temporarily make the goal buffer modifiable + modifiable = self.goal_buffer.options["modifiable"] + self.goal_buffer.options["modifiable"] = True + try: + del self.goal_buffer[:] + + response = self.coq_top.goals(feedback_callback) + + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - raw_query = ' '.join(args) + if isinstance(response, CT.Err): + return + + if response.val.val is None: + self.goal_buffer[0] = 'No goals.' + return + + goals = response.val.val + + sub_goals = goals.fg + + nb_subgoals = len(sub_goals) + plural_opt = '' if nb_subgoals == 1 else 's' + self.goal_buffer[0] = '%d subgoal%s' % (nb_subgoals, plural_opt) + self.goal_buffer.append(['']) + + for idx, sub_goal in enumerate(sub_goals): + _id = sub_goal.id + hyps = sub_goal.hyp + ccl = sub_goal.ccl + if idx == 0: + # we print the environment only for the current subgoal + for hyp in hyps: + lst = map(lambda s: s.encode('utf-8'), hyp.split('\n')) + self.goal_buffer.append(list(lst)) + self.goal_buffer.append('') + self.goal_buffer.append('======================== ( %d / %d )' % (idx+1 , nb_subgoals)) + lines = map(lambda s: s.encode('utf-8'), ccl.split('\n')) + self.goal_buffer.append(list(lines)) + self.goal_buffer.append('') + finally: + self.goal_buffer.options["modifiable"] = modifiable + + def show_info(self, message): + # Temporarily make the info buffer modifiable + modifiable = self.info_buffer.options["modifiable"] + self.info_buffer.options["modifiable"] = True + try: + del self.info_buffer[:] + lst = [] + if message is not None: + lst = list(map(lambda s: s.encode('utf-8'), + message.split('\n'))) + if len(lst) >= 1: + # If self.info_buffers was a regular list, the del statement + # above would have deleted all the lines. However with a vim + # buffer, that actually leaves 1 blank line. So now for setting + # the new contents, the very first line has to be overwritten, + # then the rest can be appended. + # + # Also note that if info_buffer was a list, extend would be the + # appropriate function. However info_buffer does not have an + # extend function, and its append mostly behaves like extend. + self.info_buffer[0] = lst[0] + self.info_buffer.append(lst[1:]) + finally: + self.info_buffer.options["modifiable"] = modifiable + + def clear_info(self): + self.coq_top.clear_errors() + self.show_info(None) + + def convert_offset(self, range_start, offset, range_end): + message = self._between(range_start, range_end) + (line, col) = _pos_from_offset(range_start[1], message, offset) + return (line + range_start[0], col) + + def reset_color(self): + sent = [] + checked = [] + warnings = [] + errors = [] + prev_end = None + sent_start = None + checked_start = None + for c in itertools.chain(self.coq_top.states): + if c.state in (CT.Command.SENT, CT.Command.ABANDONED): + if sent_start is None: + # Start a sent range + sent_start = prev_end + elif sent_start is not None: + # Finish a sent range + sent.append(make_vim_range(sent_start, prev_end)) + sent_start = None + + # Count the warning and error states as checked. A subrange will + # also be marked as a warning or error, but that will override the + # checked group. + if c.state in (CT.Command.PROCESSED, + CT.Command.WARNING, + CT.Command.ERROR): + if checked_start is None: + # Start a checked range + checked_start = prev_end + elif checked_start is not None: + # Finish a checked range + checked.append(make_vim_range(checked_start, prev_end)) + checked_start = None + prev_end = c.end + if sent_start is not None: + # Finish a sent range + sent.append(make_vim_range(sent_start, prev_end)) + if checked_start is not None: + # Finish a checked range + checked.append(make_vim_range(checked_start, prev_end)) + prev_end = None + for c in itertools.chain(self.coq_top.states, + self.coq_top.reverted_states): + if c.state in (CT.Command.WARNING, + CT.Command.ERROR): + # Normalize the start and stop positions, if it hasn't been done yet. + if c.msg_start_offset is not None and c.msg_start is None: + c.msg_start = self.convert_offset(prev_end, + c.msg_start_offset, + c.end) + if c.msg_stop_offset is not None and c.msg_stop is None: + c.msg_stop = self.convert_offset(prev_end, + c.msg_stop_offset, + c.end) + start = c.msg_start + stop = c.msg_stop + if start == stop: + start = prev_end + stop = c.end + if c.state == CT.Command.WARNING: + warnings.append(make_vim_range(start, stop)) + else: + errors.append(make_vim_range(start, stop)) + prev_end = c.end + self.source_buffer.vars['coquille_sent'] = sent + self.source_buffer.vars['coquille_checked'] = checked + self.source_buffer.vars['coquille_warnings'] = warnings + self.source_buffer.vars['coquille_errors'] = errors + vim.command("call coquille#SyncBufferColors(%d)" % + self.source_buffer.number) + + def rewind_to(self, line, col): + if self.coq_top.coqtop is None: + print('Internal error: vimbufsync is still being called but coqtop\ + appears to be down.') + print('Please report.') + return - encoding = vim.eval("&encoding") or 'utf-8' + predicate = lambda x: x.end <= (line, col) + lst = filter(predicate, self.coq_top.states) + steps = len(self.coq_top.states) - len(list(lst)) + if steps != 0: + self.coq_rewind(steps) - response = CT.query(raw_query, encoding) + ############################# + # Communication with Coqtop # + ############################# - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return + def send_until_fail(self): + """ + Tries to send every message in [send_queue] to Coq, stops at the first + error. + When this function returns, [send_queue] is empty. + """ + self.clear_info() - if isinstance(response, CT.Ok): - if response.msg is not None: - info_msg = response.msg - elif isinstance(response, CT.Err): - info_msg = response.err - else: - print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) # ugly - - show_info() - - -def launch_coq(*args): - CT.restart_coq(*args) - -def debug(): - if encountered_dots: - print("encountered dots = [") - for (line, col) in encountered_dots: - print(" (%d, %d) ; " % (line, col)) - print("]") - -##################################### -# IDE tools: Goal, Infos and colors # -##################################### - -def refresh(): - show_goal() - show_info() - reset_color() - -def show_goal(): - global info_msg - - buff = None - for b in vim.buffers: - if re.match(".*Goals$", b.name): - buff = b - break - del buff[:] - - response = CT.goals() - - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return - - if isinstance(response, CT.Ok): - if response.msg is not None: - info_msg = response.msg - elif isinstance(response, CT.Err): - if response.err is not None: - info_msg = response.err - return - - if response.val.val is None: - buff.append('No goals.') - return - - goals = response.val.val - - sub_goals = goals.fg - - nb_subgoals = len(sub_goals) - plural_opt = '' if nb_subgoals == 1 else 's' - buff.append(['%d subgoal%s' % (nb_subgoals, plural_opt), '']) - - for idx, sub_goal in enumerate(sub_goals): - _id = sub_goal.id - hyps = sub_goal.hyp - ccl = sub_goal.ccl - if idx == 0: - # we print the environment only for the current subgoal - for hyp in hyps: - lst = map(lambda s: s.encode('utf-8'), hyp.split('\n')) - buff.append(lst) - buff.append('') - buff.append('======================== ( %d / %d )' % (idx+1 , nb_subgoals)) - lines = map(lambda s: s.encode('utf-8'), ccl.split('\n')) - buff.append(lines) - buff.append('') - -def show_info(): - global info_msg - - buff = None - for b in vim.buffers: - if re.match(".*Infos$", b.name): - buff = b - break - - del buff[:] - if info_msg is not None: - lst = info_msg.split('\n') - buff.append(map(lambda s: s.encode('utf-8'), lst)) - -def clear_info(): - global info_msg - info_msg = '' - show_info() - -def reset_color(): - global error_at - # Clear current coloring (dirty) - if int(vim.eval('b:checked')) != -1: - vim.command('call matchdelete(b:checked)') - vim.command('let b:checked = -1') - if int(vim.eval('b:sent')) != -1: - vim.command('call matchdelete(b:sent)') - vim.command('let b:sent = -1') - if int(vim.eval('b:errors')) != -1: - vim.command('call matchdelete(b:errors)') - vim.command('let b:errors = -1') - # Recolor - if encountered_dots: - (line, col) = encountered_dots[-1] - start = { 'line': 0 , 'col': 0 } - stop = { 'line': line + 1, 'col': col } - zone = _make_matcher(start, stop) - vim.command("let b:checked = matchadd('CheckedByCoq', '%s')" % zone) - if len(send_queue) > 0: - (l, c) = encountered_dots[-1] if encountered_dots else (0,-1) - r = send_queue.pop() - send_queue.append(r) - (line, col) = r['stop'] - start = { 'line': l , 'col': c + 1 } - stop = { 'line': line + 1, 'col': col } - zone = _make_matcher(start, stop) - vim.command("let b:sent = matchadd('SentToCoq', '%s')" % zone) - if error_at: - ((sline, scol), (eline, ecol)) = error_at - start = { 'line': sline + 1, 'col': scol } - stop = { 'line': eline + 1, 'col': ecol } - zone = _make_matcher(start, stop) - vim.command("let b:errors = matchadd('CoqError', '%s')" % zone) - error_at = None - -def rewind_to(line, col): - if CT.coqtop is None: - print('Internal error: vimbufsync is still being called but coqtop\ - appears to be down.') - print('Please report.') - return - - predicate = lambda x: x <= (line, col) - lst = filter(predicate, encountered_dots) - steps = len(encountered_dots) - len(lst) - coq_rewind(steps) - -############################# -# Communication with Coqtop # -############################# - -def send_until_fail(): - """ - Tries to send every message in [send_queue] to Coq, stops at the first - error. - When this function returns, [send_queue] is empty. - """ - clear_info() - - global encountered_dots, error_at, info_msg - - encoding = vim.eval('&fileencoding') or 'utf-8' - - while len(send_queue) > 0: - reset_color() - vim.command('redraw') - - message_range = send_queue.popleft() - message = _between(message_range['start'], message_range['stop']) - - response = CT.advance(message, encoding) + encoding = vim.eval('&fileencoding') or 'utf-8' - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return + while len(self.send_queue) > 0: + message_range = self.send_queue.popleft() + message = self._between(message_range['start'], message_range['stop']) - if isinstance(response, CT.Ok): (eline, ecol) = message_range['stop'] - encountered_dots.append((eline, ecol + 1)) + response = self.coq_top.advance(message, + (eline, ecol + 1), encoding) + + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - optionnal_info = response.val[1] - if len(response.val) > 1 and isinstance(response.val[1], tuple): - info_msg = response.val[1][1] + if isinstance(response, CT.Ok): + optionnal_info = response.val[1] + else: + self.send_queue.clear() + if isinstance(response, CT.Err): + loc_s = response.loc_s + if loc_s is not None: + loc_e = response.loc_e + (l, c) = message_range['start'] + (l_start, c_start) = _pos_from_offset(c, message, loc_s) + (l_stop, c_stop) = _pos_from_offset(c, message, loc_e) + self.error_at = ((l + l_start, c_start), (l + l_stop, c_stop)) + else: + print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) + break + + self.reset_color() + vim.command('redraw') + + self.refresh() + + ################# + # Miscellaneous # + ################# + + def _between(self, begin, end): + """ + Returns a string corresponding to the portion of the buffer between the + [begin] and [end] positions. + """ + (bline, bcol) = begin + (eline, ecol) = end + acc = "" + for line, str in enumerate(self.source_buffer[bline:eline + 1]): + start = bcol if line == 0 else 0 + stop = ecol + 1 if line == eline - bline else len(str) + acc += str[start:stop] + '\n' + return acc + + def _get_message_range(self, after): + """ See [_find_next_chunk] """ + (line, col) = after + end_pos = self._find_next_chunk(line, col) + return { 'start':after , 'stop':end_pos } if end_pos is not None else None + + def _find_next_chunk(self, line, col): + """ + Returns the position of the next chunk dot after a certain position. + That can either be a bullet if we are in a proof, or "a string" terminated + by a dot (outside of a comment, and not denoting a path). + """ + blen = len(self.source_buffer) + bullets = ['{', '}', '-', '+', '*'] + # We start by striping all whitespaces (including \n) from the beginning of + # the chunk. + while line < blen and self.source_buffer[line][col:].strip() == '': + line += 1 + col = 0 + + if line >= blen: return + + while self.source_buffer[line][col] == ' ': # FIXME: keeping the stripped line would be + col += 1 # more efficient. + + # Then we check if the first character of the chunk is a bullet. + # Intially I did that only when I was sure to be in a proof (by looking in + # [encountered_dots] whether I was after a "collapsable" chunk or not), but + # 1/ that didn't play well with coq_to_cursor (as the "collapsable chunk" + # might not have been sent/detected yet). + # 2/ The bullet chars can never be used at the *beginning* of a chunk + # outside of a proof. So the check was unecessary. + if self.source_buffer[line][col] in bullets: + return (line, col + 1) + + # We might have a commentary before the bullet, we should be skiping it and + # keep on looking. + tail_len = len(self.source_buffer[line]) - col + if ((tail_len - 1 > 0) and self.source_buffer[line][col] == '(' + and self.source_buffer[line][col + 1] == '*'): + com_end = self._skip_comment(line, col + 2, 1) + if not com_end: return + (line, col) = com_end + return self._find_next_chunk(line, col) + + + # If the chunk doesn't start with a bullet, we look for a dot. + return self._find_dot_after(line, col) + + def _find_dot_after(self, line, col): + """ + Returns the position of the next "valid" dot after a certain position. + Valid here means: recognized by Coq as terminating an input, so dots in + comments, strings or ident paths are not valid. + """ + if line >= len(self.source_buffer): return + s = self.source_buffer[line][col:] + dot_pos = s.find('.') + com_pos = s.find('(*') + str_pos = s.find('"') + if com_pos == -1 and dot_pos == -1 and str_pos == -1: + # Nothing on this line + return self._find_dot_after(line + 1, 0) + elif dot_pos == -1 or (com_pos > - 1 and dot_pos > com_pos) or (str_pos > - 1 and dot_pos > str_pos): + if str_pos == -1 or (com_pos > -1 and str_pos > com_pos): + # We see a comment opening before the next dot + com_end = self._skip_comment(line, com_pos + 2 + col, 1) + if not com_end: return + (line, col) = com_end + return self._find_dot_after(line, col) + else: + # We see a string starting before the next dot + str_end = self._skip_str(line, str_pos + col + 1) + if not str_end: return + (line, col) = str_end + return self._find_dot_after(line, col) + elif dot_pos < len(s) - 1 and s[dot_pos + 1] != ' ': + # Sometimes dot are used to access module fields, we don't want to stop + # just after the module name. + # Example: [Require Import Coq.Arith] + return self._find_dot_after(line, col + dot_pos + 1) + elif dot_pos + col > 0 and self.source_buffer[line][col + dot_pos - 1] == '.': + # FIXME? There might be a cleaner way to express this. + # We don't want to capture ".." + if dot_pos + col > 1 and self.source_buffer[line][col + dot_pos - 2] == '.': + # But we want to capture "..." + return (line, dot_pos + col) + else: + return self._find_dot_after(line, col + dot_pos + 1) else: - send_queue.clear() - if isinstance(response, CT.Err): - info_msg = response.err - loc_s = response.loc_s - if loc_s is not None: - loc_e = response.loc_e - (l, c) = message_range['start'] - (l_start, c_start) = _pos_from_offset(c, message, loc_s) - (l_stop, c_stop) = _pos_from_offset(c, message, loc_e) - error_at = ((l + l_start, c_start), (l + l_stop, c_stop)) + return (line, dot_pos + col) + + # TODO? factorize [_skip_str] and [_skip_comment] + def _skip_str(self, line, col): + """ + Used when we encountered the start of a string before a valid dot (see + [_find_dot_after]). + Returns the position of the end of the string. + """ + while True: + if line >= len(self.source_buffer): return + s = self.source_buffer[line][col:] + str_end = s.find('"') + if str_end > -1: + return (line, col + str_end + 1) + line += 1 + col = 0 + + def _skip_comment(self, line, col, nb_left): + """ + Used when we encountered the start of a comment before a valid dot (see + [_find_dot_after]). + Returns the position of the end of the comment. + """ + while nb_left > 0: + if line >= len(self.source_buffer): return None + s = self.source_buffer[line][col:] + com_start = s.find('(*') + com_end = s.find('*)') + if com_end > -1 and (com_end < com_start or com_start == -1): + col += com_end + 2 + nb_left -= 1 + elif com_start > -1: + col += com_start + 2 + nb_left += 1 else: - print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) - break + line += 1 + col = 0 + return (line, col) - refresh() +def _empty_range(): + return [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] def _pos_from_offset(col, msg, offset): str = msg[:offset] @@ -359,211 +638,3 @@ def _pos_from_offset(col, msg, offset): line = len(lst) - 1 col = len(lst[-1]) + (col if line == 0 else 0) return (line, col) - -################# -# Miscellaneous # -################# - -def _between(begin, end): - """ - Returns a string corresponding to the portion of the buffer between the - [begin] and [end] positions. - """ - (bline, bcol) = begin - (eline, ecol) = end - buf = vim.current.buffer - acc = "" - for line, str in enumerate(buf[bline:eline + 1]): - start = bcol if line == 0 else 0 - stop = ecol + 1 if line == eline - bline else len(str) - acc += str[start:stop] + '\n' - return acc - -def _get_message_range(after): - """ See [_find_next_chunk] """ - (line, col) = after - end_pos = _find_next_chunk(line, col) - return { 'start':after , 'stop':end_pos } if end_pos is not None else None - -def _find_next_chunk(line, col): - """ - Returns the position of the next chunk dot after a certain position. - That can either be a bullet if we are in a proof, or "a string" terminated - by a dot (outside of a comment, and not denoting a path). - """ - buff = vim.current.buffer - blen = len(buff) - bullets = ['{', '}', '-', '+', '*'] - # We start by striping all whitespaces (including \n) from the beginning of - # the chunk. - while line < blen and buff[line][col:].strip() == '': - line += 1 - col = 0 - - if line >= blen: return - - while buff[line][col] == ' ': # FIXME: keeping the stripped line would be - col += 1 # more efficient. - - # Then we check if the first character of the chunk is a bullet. - # Intially I did that only when I was sure to be in a proof (by looking in - # [encountered_dots] whether I was after a "collapsable" chunk or not), but - # 1/ that didn't play well with coq_to_cursor (as the "collapsable chunk" - # might not have been sent/detected yet). - # 2/ The bullet chars can never be used at the *beginning* of a chunk - # outside of a proof. So the check was unecessary. - if buff[line][col] in bullets: - return (line, col + 1) - - # We might have a commentary before the bullet, we should be skiping it and - # keep on looking. - tail_len = len(buff[line]) - col - if (tail_len - 1 > 0) and buff[line][col] == '(' and buff[line][col + 1] == '*': - com_end = _skip_comment(line, col + 2, 1) - if not com_end: return - (line, col) = com_end - return _find_next_chunk(line, col) - - - # If the chunk doesn't start with a bullet, we look for a dot. - return _find_dot_after(line, col) - -def _find_dot_after(line, col): - """ - Returns the position of the next "valid" dot after a certain position. - Valid here means: recognized by Coq as terminating an input, so dots in - comments, strings or ident paths are not valid. - """ - b = vim.current.buffer - if line >= len(b): return - s = b[line][col:] - dot_pos = s.find('.') - com_pos = s.find('(*') - str_pos = s.find('"') - if com_pos == -1 and dot_pos == -1 and str_pos == -1: - # Nothing on this line - return _find_dot_after(line + 1, 0) - elif dot_pos == -1 or (com_pos > - 1 and dot_pos > com_pos) or (str_pos > - 1 and dot_pos > str_pos): - if str_pos == -1 or (com_pos > -1 and str_pos > com_pos): - # We see a comment opening before the next dot - com_end = _skip_comment(line, com_pos + 2 + col, 1) - if not com_end: return - (line, col) = com_end - return _find_dot_after(line, col) - else: - # We see a string starting before the next dot - str_end = _skip_str(line, str_pos + col + 1) - if not str_end: return - (line, col) = str_end - return _find_dot_after(line, col) - elif dot_pos < len(s) - 1 and s[dot_pos + 1] != ' ': - # Sometimes dot are used to access module fields, we don't want to stop - # just after the module name. - # Example: [Require Import Coq.Arith] - return _find_dot_after(line, col + dot_pos + 1) - elif dot_pos + col > 0 and b[line][col + dot_pos - 1] == '.': - # FIXME? There might be a cleaner way to express this. - # We don't want to capture ".." - if dot_pos + col > 1 and b[line][col + dot_pos - 2] == '.': - # But we want to capture "..." - return (line, dot_pos + col) - else: - return _find_dot_after(line, col + dot_pos + 1) - else: - return (line, dot_pos + col) - -# TODO? factorize [_skip_str] and [_skip_comment] -def _skip_str(line, col): - """ - Used when we encountered the start of a string before a valid dot (see - [_find_dot_after]). - Returns the position of the end of the string. - """ - b = vim.current.buffer - if line >= len(b): return - s = b[line][col:] - str_end = s.find('"') - if str_end > -1: - return (line, col + str_end + 1) - else: - return _skip_str(line + 1, 0) - -def _skip_comment(line, col, nb_left): - """ - Used when we encountered the start of a comment before a valid dot (see - [_find_dot_after]). - Returns the position of the end of the comment. - """ - if nb_left == 0: - return (line, col) - - b = vim.current.buffer - if line >= len(b): return - s = b[line][col:] - com_start = s.find('(*') - com_end = s.find('*)') - if com_end > -1 and (com_end < com_start or com_start == -1): - return _skip_comment(line, col + com_end + 2, nb_left - 1) - elif com_start > -1: - return _skip_comment(line, col + com_start + 2, nb_left + 1) - else: - return _skip_comment(line + 1, 0, nb_left) - -def _will_be_collapsed(s): - """ - Collapsable part are useful when we want to rewind to a certain position. - Indeed when we send something to Coq, a "step" is just a string between two - "valid" dots, but when we rewind a step might be /bigger/ than that as Coq - doesn't rewind just a "Qed" or "Defined" when it meets one, but the whole - proof (returning the "actual" number of steps rewinded). - We could just rewind one step at a time until we reach the desired point in - the buffer, but this seems more efficient. - """ - if re.match(".*(Theorem|Goal|Lemma|Next Obligation).*", s): - return True - elif re.match('.*Definition .*', s) and not re.search(':=', s): - return True - else: - return False - -def _time_to_collapse(s): - """ Used in conjunction with [_will_be_collapsed] """ - return True if re.match('.*(Qed|Defined)\.$', s) else False - -## I thought python was the language with a big stdlib... -def rfind(lst, cond): - tmp = None - for idx, elt in enumerate(lst): - if cond(elt): tmp = idx - return tmp - -################################################ -# The ugly through behind regions highlighting # -################################################ - -def _make_matcher(start, stop): - if start['line'] == stop['line']: - return _easy_matcher(start, stop) - else: - return _hard_matcher(start, stop) - -def _easy_matcher(start, stop): - startl = "" - startc = "" - if start['line'] > 0: - startl = "\%>{0}l".format(start['line'] - 1) - if start['col'] > 0: - startc = "\%>{0}c".format(start['col']) - return '{0}{1}\%<{2}l\%<{3}c'.format(startl, startc, stop['line'] + 1, stop['col'] + 1) - -def _hard_matcher(start, stop): - first_start = {'line' : start['line'], 'col' : start['col']} - first_stop = {'line' : start['line'], 'col' : 4242} - first_line = _easy_matcher(first_start, first_stop) - mid_start = {'line' : start['line']+1, 'col' : 0} - mid_stop = {'line' : stop['line']-1 , 'col' : 4242} - middle = _easy_matcher(mid_start, mid_stop) - last_start = {'line' : stop['line'], 'col' : 0} - last_stop = {'line' : stop['line'], 'col' : stop['col']} - last_line = _easy_matcher(last_start, last_stop) - return "{0}\|{1}\|{2}".format(first_line, middle, last_line) diff --git a/autoload/coquille.vim b/autoload/coquille.vim index 0e5045f..68a8bc4 100644 --- a/autoload/coquille.vim +++ b/autoload/coquille.vim @@ -1,12 +1,76 @@ -let s:coq_running=0 +" When set to 1, new coq source windows will try to use a info and goals +" window in the same tab. When set to 0, they will create their own info and +" goals windows. +" +" This can be overriden in a source window by setting w:coquille_shared. +let g:coquille_shared = 1 +" When set to 1, keep the infos and goals windows open after they are no +" longer referenced. This is useful if you arranged the coq windows in a +" specific way, and you keep switching between coq and non-coq files without +" using the hidden option. +" +" This can be overriden in a source window by setting w:coquille_keep_open. +let g:coquille_keep_open = 0 +" When set to 1, read the coqtop arguments from _CoqProject, and append them to +" the arguments passed by CoqLaunch when calling coqtop. +" +" This can be overriden in a source buffer by setting +" b:coquille_append_project_args. +let g:coquille_append_project_args = 1 + let s:current_dir=expand(":p:h") +let s:next_winid = 1 +let s:active_winid = -1 +let s:active_tabnr = -1 +let s:active_winnr = -1 if !exists('coquille_auto_move') let g:coquille_auto_move="false" endif +" Return true if win_getid works +function! coquille#Test_win_getid() + if !exists("*win_getid") + return 0 + endif + + " At least the function exists. + " + " Fedora 23 has a broken version that only works if the tab argument is + " left off. When the tab argument is included, it always returns 0. + " + " So test win_getid() by trying to get the id of the current window. + let s:curid = win_getid(tabpagenr(), winnr()) + if s:curid == 0 || s:curid == -1 + return 0 + endif + " All tests passed. The system win_getid() function works. + return 1 +endfunction + +" Cache whether win_getid works +let s:win_getid_works = coquille#Test_win_getid() + +function! coquille#Python(cmd) + if has('python3') + execute 'python3' a:cmd + else + execute 'python' a:cmd + endif +endfunction + +function! coquille#PythonExpr(expr) + let l:ret = 0 + if has('python3') + execute 'python3 vim.command("let l:ret = " + coquille.vim_repr(' a:expr '))' + else + execute 'python vim.command("let l:ret = " + coquille.vim_repr(' a:expr '))' + endif + return l:ret +endfunction + try - py import sys, vim + call coquille#Python('import sys, vim') catch /E319:/ if !exists('s:warned') echo "vim doesn't support python. Turn off coquille" @@ -17,43 +81,12 @@ catch /E319:/ finish endtry - " Load vimbufsync if not already done call vimbufsync#init() -py if not vim.eval("s:current_dir") in sys.path: -\ sys.path.append(vim.eval("s:current_dir")) -py import coquille - -function! coquille#ShowPanels() - " open the Goals & Infos panels before going back to the main window - let l:winnb = winnr() - rightbelow vnew Goals - setlocal buftype=nofile - setlocal filetype=coq-goals - setlocal noswapfile - let s:goal_buf = bufnr("%") - rightbelow new Infos - setlocal buftype=nofile - setlocal filetype=coq-infos - setlocal noswapfile - let s:info_buf = bufnr("%") - execute l:winnb . 'winc w' -endfunction - -function! coquille#KillSession() - let s:coq_running = 0 - - execute 'bdelete' . s:goal_buf - execute 'bdelete' . s:info_buf - py coquille.kill_coqtop() - - setlocal ei=InsertEnter -endfunction - -function! coquille#RawQuery(...) - py coquille.coq_raw_query(*vim.eval("a:000")) -endfunction +call coquille#Python('if not vim.eval("s:current_dir") in sys.path:'. + \'sys.path.append(vim.eval("s:current_dir"))') +call coquille#Python('import coquille') function! coquille#FNMapping() "" --- Function keys bindings @@ -82,26 +115,104 @@ function! coquille#CoqideMapping() imap :CoqToCursor endfunction -function! coquille#Launch(...) - if s:coq_running == 1 - echo "Coq is already running" - else - let s:coq_running = 1 +" Create a new, unlisted, unloaded buffer, with a name starting with base_name +function! coquille#CreateNewBuffer(base_name) + if !bufexists(a:base_name) + return bufnr(a:base_name, 1) + endif + let l:suffix = 1 + while bufexists(a:base_name . l:suffix) + let l:suffix += 1 + endwhile + return bufnr(a:base_name . l:suffix, 1) +endfunction - " initialize the plugin (launch coqtop) - py coquille.launch_coq(*vim.eval("map(copy(a:000),'expand(v:val)')")) +" Detach any goal and info buffer attached the coq source buffer. +function! coquille#DetachSupportingBuffers(bufid) + for type in ["goal", "info"] + let l:varname = "coquille_" . type . "_bufid" + let l:support_bufid = getbufvar(a:bufid, l:varname, -1) + if bufexists(l:support_bufid) + call setbufvar(l:support_bufid, "&bufhidden", "delete") + endif + call setbufvar(a:bufid, l:varname, -1) + endfor + call coquille#Python('coquille.BufferState.lookup_bufid(' . a:bufid . ').' . + \ 'kill_coqtop()') +endfunction - " make the different commands accessible - command! -buffer GotoDot py coquille.goto_last_sent_dot() - command! -buffer CoqNext py coquille.coq_next() - command! -buffer CoqUndo py coquille.coq_rewind() - command! -buffer CoqToCursor py coquille.coq_to_cursor() - command! -buffer CoqKill call coquille#KillSession() +function! coquille#KillSession() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#TabWinBufnr(tabpagenr(), winnr()) - command! -buffer -nargs=* Coq call coquille#RawQuery() + call coquille#DetachSupportingBuffers(l:bufid) - call coquille#ShowPanels() + " Reactive the coq source window now that its current buffer is no longer + " a coq source. This will close the support windows if nothing else is + " referencing them. + call coquille#WindowActivated(l:winid, tabpagenr(), winnr()) + setlocal ei=InsertEnter +endfunction + +" If they do not already exist, create a goals and infos buffer for coq source, +" bufid. +function! coquille#OpenSupportingBuffers(bufid, ...) + if !bufloaded(a:bufid) + return + endif + if getbufvar(a:bufid, "&filetype") != "coq" + return + endif + let l:created_bufs = 0 + for type in ["goal", "info"] + " Skip this buffer type if b:coquille_goal_bufid/b:coquille_info_bufid + " is set on the coq source buffer, and it points to a loaded buffer + let l:varname = "coquille_" . type . "_bufid" + let l:support_bufid = getbufvar(a:bufid, l:varname, -1) + if bufexists(l:support_bufid) + continue + endif + + if type == "goal" + let l:bufname_base = "Goals: ".bufname("%") + else + let l:bufname_base = "Infos: ".bufname("%") + endif + let l:support_bufid = coquille#CreateNewBuffer(l:bufname_base) + + " In the support window, do (setlocal nomodifiable). This prevents the + " user from accidentally editing the contents. + call setbufvar(l:support_bufid, "&modifiable", 0) + " In the support window, do (setlocal buftype=nofile). This way even + " if the buffer is modified, the modified option won't get set. + call setbufvar(l:support_bufid, "&buftype", "nofile") + " In the support window, set the filetype directly, and store it to + " coquille_filetype. If the filefile type gets overwritten later, the + " file type detector will restore it from b:coquille_filetype. + let l:filetype = "coq-".type."s" + call setbufvar(l:support_bufid, "coquille_filetype", l:filetype) + call setbufvar(l:support_bufid, "&filetype", l:filetype) + " In the support window, do (setlocal noswapfile). This way if vim + " exits uncleanly, on the next start up the user won't be asked to + " restore the info/goals files. + call setbufvar(l:support_bufid, "&swapfile", 0) + call setbufvar(l:support_bufid, "&bufhidden", "hide") + call setbufvar(l:support_bufid, "coquille_source_bufid", a:bufid) + " Add it to the buffer list + call setbufvar(l:support_bufid, "&buflisted", 1) + + " Set b:coquille_goal_bufid/b:coquille_info_bufid on the coq source + " buffer. + call setbufvar(a:bufid, l:varname, l:support_bufid) + let l:created_bufs += 1 + endfor + if l:created_bufs + call setbufvar(a:bufid, "checked", -1) + call setbufvar(a:bufid, "sent", -1) + call setbufvar(a:bufid, "errors", -1) + execute "autocmd BufUnload call coquille#DetachSupportingBuffers(". a:bufid .")" " 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. @@ -109,18 +220,643 @@ function! coquille#Launch(...) " delete some part of your buffer. So the highlighting will be wrong, but " nothing really problematic will happen, as sync will be called the next " time you explicitly call a command (be it 'rewind' or 'interp') - au InsertEnter py coquille.sync() + execute "autocmd InsertEnter call coquille#Python('" + \ "coquille.BufferState.lookup_bufid(". + \ a:bufid . ").sync()')" + " initialize the plugin (launch coqtop) + let l:result = coquille#PythonExpr( + \ 'coquille.BufferState.lookup_bufid(' . + \ a:bufid . ').launch_coq(' . + \ '*' . string(map(copy(a:000), 'expand(v:val)')) . ')') + if !l:result + " Since coq failed to launch, delete the buffers created above + execute "bdelete" getbufvar(a:bufid, "coquille_goal_bufid") + \ getbufvar(a:bufid, "coquille_info_bufid") + call coquille#DetachSupportingBuffers(a:bufid) + return 0 + endif endif + return 1 endfunction -function! coquille#Register() - hi default CheckedByCoq ctermbg=17 guibg=LightGreen - hi default SentToCoq ctermbg=60 guibg=LimeGreen +function! coquille#WinGetId(tabnr, winnr) + if s:win_getid_works + return win_getid(a:winnr, a:tabnr) + endif + let l:winid = gettabwinvar(a:tabnr, a:winnr, "coquille_winid", -1) + if l:winid != -1 + return l:winid + endif + let l:winid = s:next_winid + let s:next_winid += 1 + call settabwinvar(a:tabnr, a:winnr, "coquille_winid", l:winid) + return l:winid +endfunction + +" Return the [tabnr, winnr] for a given window id. +" +" If the window id cannot be found, [0, 0] is returned. +" +" Passing a close value in [hint_tabnr, winnr] speeds up the search +function! coquille#WinId2TabWin(winid, hint_tabnr, hint_winnr) + " win_id2tabwin was introduced in vim 8. Use it if it is available. + if s:win_getid_works + return win_id2tabwin(a:winid) + endif + if gettabwinvar(a:hint_tabnr, a:hint_winnr, "coquille_winid", -1) == a:winid + " If this matches and the hint_tabnr or hint_winnr is 0, that means + " the current tab/window is a match. However the caller is expecting + " the real tab and window numbers, so they have to be converted. + let l:tabnr = a:hint_tabnr + if l:tabnr == 0 + let l:tabnr = tabpagenr() + endif + let l:winnr = a:hint_winnr + if l:winnr == 0 + let l:winnr = winnr() + endif + return [l:tabnr, l:winnr] + endif + let l:search_tab=1 + while l:search_tab <= tabpagenr("$") + let l:search_win=1 + while l:search_win <= tabpagewinnr(l:search_tab, "$") + if gettabwinvar(l:search_tab, l:search_win, "coquille_winid", -1) + \ == a:winid + return [l:search_tab, l:search_win] + endif + let l:search_win += 1 + endwhile + let l:search_tab += 1 + endwhile + return [0, 0] +endfunction + +" Return the window variable in the given window id, or default if the window +" or variable does not exist +" +" Specifying a hint_tabnr and hint_winnr that matches the winid speeds up the +" search. +function! coquille#GetWinVar(winid, hint_tabnr, hint_winnr, varname, def) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + return gettabwinvar(l:tabwin[0], l:tabwin[1], a:varname, a:def) +endfunction + +" Set the window variable in the given window id to the given value, if the +" window exists +" +" Specifying a hint_tabnr and hint_winnr that matches the winid speeds up the +" search. +function! coquille#SetWinVar(winid, hint_tabnr, hint_winnr, varname, value) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + call settabwinvar(l:tabwin[0], l:tabwin[1], a:varname, a:value) +endfunction + +" Return true if the window is open +function! coquille#WinIdExists(winid, hint_tabnr, hint_winnr) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + return l:tabwin[0] != 0 || l:tabwin[1] != 0 +endfunction + +function! coquille#WinVarExists(winid, hint_tabnr, hint_winnr, varname) + let l:value1 = coquille#GetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ a:varname, -1) + let l:value2 = coquille#GetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ a:varname, -2) + return l:value1 == l:value2 +endfunction + +function! coquille#CloseWindow(winid, hint_tabnr, hint_winnr) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + " Only try close the window if it exists + if l:tabwin[0] != 0 || l:tabwin[1] != 0 + let l:close_bufid = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) + " The only way to close a window in a different tab is to switch to + " it. Save the current tab so it can be restored later. + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + " Switch to the tab + execute l:tabwin[0] . " tabnext" + " Vim uses the bufhidden variable from the active buffer. Really it + " should use the bufhidden variable from the window that is getting + " closed. So as a workaround, temporarily copy the value from the + " closing buffer to the active buffer. + let l:cur_bufid = bufnr("") + let l:bufhidden_backup = &bufhidden + let &bufhidden = getbufvar(l:close_bufid, "&bufhidden") + " Quit the window + execute l:tabwin[1] . " wincmd q" + " Switch back to the original tab + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) + " Restore the old value of the bufhidden variable + call setbufvar(l:cur_bufid, "&bufhidden", l:bufhidden_backup) + endif +endfunction + +" Make winid current by changing the current tab and window within that tab +function! coquille#WinGoToId(winid, hint_tabnr, hint_winnr) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + if l:tabwin[0] == 0 && l:tabwin[1] == 0 + return 0 + else + execute l:tabwin[0] . " tabnext" + execute l:tabwin[1] . " wincmd w" + return 1 + endif +endfunction + +" Return the active buffer number for the given tab and window +function! coquille#TabWinBufnr(tabnr, winnr) + return tabpagebuflist(a:tabnr)[a:winnr - 1] +endfunction + +" Return the active buffer number for the given winid +function! coquille#WinidBufnr(winid) + if s:win_getid_works + return getwininfo(a:winid)[0].bufnr + endif + let l:tabwin = coquille#WinId2TabWin(a:winid, 0, 0) + return coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) +endfunction + +" Load the given buffer in the given window +function! coquille#SetWinBufnr(winid, hint_tabnr, hint_winnr, bufid) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + let l:target_bufid = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) + if a:bufid == l:target_bufid + " The buffer is already active in the target window + return + endif + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + " Go to the target window + call coquille#WinGoToId(a:winid, l:tabwin[0], l:tabwin[1]) + execute a:bufid . " buffer" + " Restore the previous active window + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) +endfunction + +" Return the list of all windows that are showing bufid as a list of winids +function! coquille#WinFindBuf(bufid) + if s:win_getid_works + return win_findbuf(a:bufid) + endif + let winlist = [] + for tabnr in range(1, tabpagenr('$')) + let l:tabwins = tabpagebuflist(l:tabnr) + for i in range(len(l:tabwins)) + let l:winnr = i + 1 + if a:bufid == l:tabwins[i] + call add(l:winlist, coquille#WinGetId(l:tabnr, l:winnr)) + endif + endfor + endfor + return l:winlist +endfunction + +" Return the window id of a window in the specified tab with the specified +" filetype, with w:coquille_shared set to 1, or -1 if no such window exists +function! coquille#FindSharedWin(tabnr, filetype) + let l:search_win=1 + let l:default_shared = !exists("g:coquille_shared") || g:coquille_shared + while l:search_win <= tabpagewinnr(a:tabnr, "$") + if !gettabwinvar(a:tabnr, l:search_win, "coquille_shared", + \ l:default_shared) + let l:search_win += 1 + continue + endif + let bufid = coquille#TabWinBufnr(a:tabnr, l:search_win) + if getbufvar(l:bufid, "&filetype") != a:filetype + let l:search_win += 1 + continue + endif + return coquille#WinGetId(a:tabnr, l:search_win) + endwhile + return -1 +endfunction + +function coquille#LoadBlankBuffer(winid, hint_tabnr, hint_winnr) + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + " Go to the target window + call coquille#WinGoToId(a:winid, a:hint_tabnr, a:hint_winnr) + enew + setlocal buftype=nofile + setlocal noswapfile + " Restore the previous active window + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) +endfunction + +" Close the info/goal window if coquille_keep_open is false and there are no +" more source windows referencing the support window in the tab +" +" If the window says open, load an empty buffer in it +function coquille#GarbageCollectSupportWin(winid) + let l:tabwin = coquille#WinId2TabWin(a:winid, 0, 0) + if l:tabwin[0] == 0 && l:tabwin[1] == 0 + " The support window doesn't exist + return + endif + let l:def_keep_open = 0 + if exists("g:coquille_keep_open") + let l:def_keep_open = g:coquille_keep_open + endif + if coquille#GetWinVar(a:winid, l:tabwin[0], l:tabwin[1], + \ "coquille_keep_open", l:def_keep_open) + call coquille#LoadBlankBuffer(a:winid, l:tabwin[0], l:tabwin[1]) + return + endif + let l:search_win=1 + while l:search_win <= tabpagewinnr(l:tabwin[0], "$") + if gettabwinvar(l:tabwin[0], l:search_win, "coquille_goal_winid", -1) + \ == a:winid || + \ gettabwinvar(l:tabwin[0], l:search_win, + \ "coquille_info_winid", -1) + \ == a:winid + " Found a source window that still references the support window. + " Now see if that source window has a source buffer. + let l:search_bufid = coquille#TabWinBufnr(l:tabwin[0], l:search_win) + let l:search_goal_bufid = getbufvar(l:search_bufid, + \ "coquille_goal_bufid", -1) + let l:search_info_bufid = getbufvar(l:search_bufid, + \ "coquille_info_bufid", -1) + if bufexists(l:search_goal_bufid) && bufexists(l:search_info_bufid) + " The window can't be closed because the source buffer is + " still using it. However that source buffer is not active, so + " put a blank buffer in the support window instead. + call coquille#LoadBlankBuffer(a:winid, l:tabwin[0], l:tabwin[1]) + return + endif + endif + let l:search_win += 1 + endwhile + call coquille#CloseWindow(a:winid, l:tabwin[0], l:tabwin[1]) +endfunction + +" Create/swap buffers/close the goals and info windows attached to a coq +" source window. +function! coquille#UpdateSupportingWindows(winid, hint_tabnr, hint_winnr) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + let l:bufid = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) + let l:goal_winid = coquille#GetWinVar(a:winid, l:tabwin[0], + \ l:tabwin[1], + \ "coquille_goal_winid", -1) + let l:info_winid = coquille#GetWinVar(a:winid, l:tabwin[0], + \ l:tabwin[1], + \ "coquille_info_winid", -1) + if getbufvar(l:bufid, "coquille_block_activate", 0) + " An autocmd recursively called this function while the window was + " already getting activated + return + endif + call setbufvar(l:bufid, "coquille_block_activate", 1) + + let l:goal_bufid = getbufvar(l:bufid, "coquille_goal_bufid", -1) + let l:info_bufid = getbufvar(l:bufid, "coquille_info_bufid", -1) + if l:goal_bufid != -1 && l:info_bufid != -1 + " The requested window has a coq source buffer. If the source has + " corresponding info and goal buffers, make sure they are displayed in + " the goal and info windows. The goal and info windows are created if + " necessary. + if !coquille#WinIdExists(l:goal_winid, 0, 0) + let l:goal_winid = -1 + endif + if !coquille#WinIdExists(l:info_winid, 0, 0) + let l:info_winid = -1 + endif + " Creating new windows involves switching the current window and tab. + " Save the current values so they can be restored at the end + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + + if l:goal_winid == -1 + " See if there is a shared goals window in the current tab that + " can be used + let l:goal_winid = coquille#FindSharedWin(l:tabwin[0], "coq-goals") + if l:goal_winid != -1 + call coquille#SetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_goal_winid", l:goal_winid) + endif + endif + if l:goal_winid == -1 + let l:goal_name = bufname(l:goal_bufid) + if l:info_winid == -1 + " The goals and info windows do not exist. + " First go to the source's tab and window + execute l:tabwin[0] . " tabnext" + execute l:tabwin[1] . " wincmd w" + " Create the goals window to the right of the source window, + " and load the goals buffer + execute "rightbelow vsplit " . fnameescape(bufname(l:goal_name)) + else + " The goals window does not exist, but the info window does exist. + " First go to the info's tab and window + call coquille#WinGoToId(l:info_winid, 0, 0) + " Create the goals window above the info window, and load the + " goals buffer + execute "leftabove split " . fnameescape(bufname(l:goal_name)) + endif + let l:goal_winid = coquille#WinGetId(tabpagenr(), winnr()) + if coquille#WinVarExists(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_shared") + " The goals window inherits w:coquille_shared from the + " source window. + let w:coquille_shared = + \ coquille#GetWinVar(a:winid, a:hint_tabnr, + \ a:hint_winnr, + \ "coquille_shared", "") + endif + call coquille#SetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_goal_winid", l:goal_winid) + endif + if l:info_winid == -1 + " See if there is a shared info window in the current tab that + " can be used. Refresh l:tabwin in case a new tab or window was + " created above that messed up the numbers. + let l:tabwin = coquille#WinId2TabWin(a:winid, l:tabwin[0], + \ l:tabwin[1]) + let l:info_winid = coquille#FindSharedWin(l:tabwin[0], "coq-infos") + if l:info_winid != -1 + call coquille#SetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_info_winid", l:info_winid) + endif + endif + if l:info_winid == -1 + " The info window does not exist, but the goals window has to + " exist because it was created above if necessary. + let l:info_name = bufname(l:info_bufid) + " First go to the goals window. + let l:goal_tabwin = coquille#WinId2TabWin(l:goal_winid, tabpagenr(), + \ winnr()) + execute l:goal_tabwin[0] . " tabnext" + execute l:goal_tabwin[1] . " wincmd w" + " Create the info window below the goals window, and load the + " info buffer. + execute "rightbelow split " . fnameescape(bufname(l:info_name)) + let l:info_winid = coquille#WinGetId(tabpagenr(), winnr()) + if coquille#WinVarExists(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_shared") + " The info window inherits w:coquille_shared from the + " source window. + let w:coquille_shared = + \ coquille#GetWinVar(a:winid, a:hint_tabnr, + \ a:hint_winnr, + \ "coquille_shared", "") + endif + call coquille#SetWinVar(a:winid, a:hint_tabnr, a:hint_winnr, + \ "coquille_info_winid", l:info_winid) + endif + " Restore the active window + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) + " In case the goal and info windows were not created above, put the + " correct buffers in them + call coquille#SetWinBufnr(l:goal_winid, 0, 0, l:goal_bufid) + call coquille#SetWinBufnr(l:info_winid, 0, 0, l:info_bufid) + else + call coquille#GarbageCollectSupportWin(l:goal_winid) + call coquille#GarbageCollectSupportWin(l:info_winid) + endif + call setbufvar(l:bufid, "coquille_block_activate", 0) +endfunction + +" Create the pattern string to match from start until stop +" +" start and stop are in the format: [line, col]. +" +" The lines and columns are 1-based. The start position is included in the +" match (unless excluded by stop), and the final column in the stop position +" is excluded. +" +" For the stop position, a line of -1 means highlight until the end of the +" file. A column of -1 means highlight until the end of the specified line. +function! coquille#GetRangePattern(start, stop) + if a:start[0] > a:stop[0] + let l:pattern = '' + elseif a:start[0] == a:stop[0] + " Start the pattern by matching anything on the start line + let l:pattern = printf('\%%%dl', a:start[0]) + if a:start[1] > 1 + " Refine the pattern to only match columns > (start[1]-1). + let l:pattern .= printf('\%%>%dc', a:start[1] - 1) + endif + if a:stop[1] != -1 + " Refine the pattern to only match columns < (stop[1]). + let l:pattern .= printf('\%%<%dc', a:stop[1]) + endif + else + " Start the pattern by matching anything on the start line + let l:pattern = printf('\%%%dl', a:start[0]) + if a:start[1] > 1 + " Refine the pattern to only match columns > (start[1]-1) on + " the first line. + let l:pattern .= printf('\%%>%dc', a:start[1] - 1) + endif + " Create a new branch in the pattern which matches any column of the + " lines [start[0] + 1, stop[0] - 1] (bounds included). + " + " Create one more branch that matches any column in stop[0]. + let l:pattern .= printf('\|\%%>%dl\%%<%dl\|\%%%dl', + \ a:start[0], + \ a:stop[0], + \ a:stop[0]) + if a:stop['col'] != -1 + " Refine that last branch to only match columns < (stop[1]). + let l:pattern .= printf('\%%<%dc', a:stop[1]) + endif + endif + return l:pattern +endfunction + +function! coquille#GetRangeListPattern(lst) + return join(map(copy(a:lst), + \ 'coquille#GetRangePattern(v:val[0], v:val[1])'), + \ '\|') +endfunction + +let s:empty_range = [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] + +function! coquille#SyncWindowColors(winid, hint_tabnr, hint_winnr) + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + let l:bufnr = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) + " Map from variable name to [group name, priority] + let l:group_infos = { + \ "coquille_checked": ["CheckedByCoq", 10], + \ "coquille_sent": ["SentToCoq", 10], + \ "coquille_errors": ["CoqError", 11], + \ "coquille_warnings": ["CoqWarning", 11] + \ } + + let l:switched = 0 + for group in keys(l:group_infos) + let l:win_value = coquille#GetWinVar(a:winid, l:tabwin[0], l:tabwin[1], + \ l:group, [s:empty_range, -1]) + let l:buf_value = getbufvar(l:bufnr, l:group, s:empty_range) + if l:win_value[0] == l:buf_value + " It already matches; nothing to do + continue + endif + " matchadd() only works for the current window. So switch to a:winid. + if !l:switched + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + call coquille#WinGoToId(a:winid, l:tabwin[0], l:tabwin[1]) + endif + if l:win_value[1] != -1 + call matchdelete(l:win_value[1]) + endif + if l:buf_value == s:empty_range + let l:matchid = -1 + else + let l:group_info = l:group_infos[l:group] + let l:matchid = matchadd(l:group_info[0], + \ coquille#GetRangeListPattern(l:buf_value), + \ l:group_info[1]) + endif + call coquille#SetWinVar(a:winid, l:tabwin[0], l:tabwin[1], + \ l:group, [l:buf_value, l:matchid]) + endfor + if l:switched + " Switch back to the original tab + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) + endif +endfunction + +function! coquille#SyncBufferColors(bufid) + for winid in coquille#WinFindBuf(a:bufid) + call coquille#SyncWindowColors(l:winid, 0, 0) + endfor +endfunction + +function! coquille#WindowActivated(winid, hint_tabnr, hint_winnr) + " If there was a previously active coquille window, and it was closed, + " then its support windows need to be closed too + if s:active_winid != -1 + if !coquille#WinIdExists(s:active_winid, s:active_tabnr, s:active_winnr) + " The source window was closed, so close the support windows + call coquille#GarbageCollectSupportWin(s:active_goal_winid) + call coquille#GarbageCollectSupportWin(s:active_info_winid) + endif + endif + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + let l:goal_winid = coquille#GetWinVar(a:winid, l:tabwin[0], + \ l:tabwin[1], + \ "coquille_goal_winid", -1) + let l:info_winid = coquille#GetWinVar(a:winid, l:tabwin[0], + \ l:tabwin[1], + \ "coquille_info_winid", -1) + if l:goal_winid != -1 && l:info_winid != -1 + let s:active_winid = a:winid + let s:active_tabnr = l:tabwin[0] + let s:active_winnr = l:tabwin[1] + let s:active_goal_winid = l:goal_winid + let s:active_info_winid = l:info_winid + endif + call coquille#UpdateSupportingWindows(a:winid, l:tabwin[0], l:tabwin[1]) + call coquille#SyncWindowColors(a:winid, l:tabwin[0], l:tabwin[1]) +endfunction + +function! coquille#EnsureLaunched(winid, ...) + " The colors are set as late as possible to give the background option + " more time to get set. + if &background == 'dark' + hi default CheckedByCoq ctermbg=22 guibg=DarkGreen + hi default SentToCoq ctermbg=65 guibg=DarkOliveGreen + hi default CoqWarning ctermbg=94 guibg=goldenrod4 + else + hi default CheckedByCoq ctermbg=22 guibg=DarkGreen + hi default CheckedByCoq ctermbg=120 guibg=LightGreen + hi default SentToCoq ctermbg=77 guibg=LimeGreen + hi default CoqWarning ctermbg=220 guibg=gold + endif hi link CoqError Error + let l:tabwin = coquille#WinId2TabWin(a:winid, tabpagenr(), winnr()) + let l:bufid = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) + if ! call(function("coquille#OpenSupportingBuffers"), + \ extend([l:bufid], a:000)) + return -1 + endif + call coquille#WindowActivated(a:winid, l:tabwin[0], l:tabwin[1]) + return l:bufid +endfunction + +function! coquille#Launch(...) + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#TabWinBufnr(tabpagenr(), winnr()) + let l:goal_bufid = getbufvar(l:bufid, "coquille_goal_bufid", -1) + let l:info_bufid = getbufvar(l:bufid, "coquille_info_bufid", -1) + if l:goal_bufid != -1 && l:info_bufid != -1 + echo "Coq is already running" + else + call call(function("coquille#EnsureLaunched"), + \ extend([l:winid], a:000)) + endif +endfunction + +function! coquille#GotoLastSentDot() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#EnsureLaunched(l:winid) + call coquille#Python('coquille.BufferState.lookup_bufid(' . l:bufid . ').' . + \ '.goto_last_sent_dot()') +endfunction + +function! coquille#CoqNext() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#EnsureLaunched(l:winid) + call coquille#Python('coquille.BufferState.lookup_bufid(' . l:bufid . ').' . + \ 'coq_next()') +endfunction + +function! coquille#CoqRewind() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#EnsureLaunched(l:winid) + call coquille#Python('coquille.BufferState.lookup_bufid(' . l:bufid . ').' . + \ 'coq_rewind()') +endfunction + +function! coquille#CoqToCursor() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#EnsureLaunched(l:winid) + call coquille#Python('coquille.BufferState.lookup_bufid(' . l:bufid . ').' . + \ 'coq_to_cursor()') +endfunction + +function! coquille#RawQuery(...) + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#EnsureLaunched(l:winid) + call coquille#Python('coquille.BufferState.lookup_bufid(' . l:bufid . ').' . + \ 'coq_raw_query(*'. string(a:000) . ')') +endfunction + +function! coquille#Register() let b:checked = -1 let b:sent = -1 let b:errors = -1 + " make the different commands accessible + command! -buffer GotoDot call coquille#GotoLastSentDot() + command! -buffer CoqNext call coquille#CoqNext() + command! -buffer CoqUndo call coquille#CoqRewind() + command! -buffer CoqToCursor call coquille#CoqToCursor() + command! -buffer CoqKill call coquille#KillSession() + + command! -buffer -nargs=* Coq call coquille#RawQuery() + command! -bar -buffer -nargs=* -complete=file CoqLaunch call coquille#Launch() + + augroup coquille + autocmd! + autocmd WinEnter * call coquille#WindowActivated( + \ coquille#WinGetId(tabpagenr(), winnr()), + \ tabpagenr(), winnr()) + autocmd BufWinEnter * call coquille#WindowActivated( + \ coquille#WinGetId(tabpagenr(), winnr()), + \ tabpagenr(), winnr()) + augroup END endfunction diff --git a/autoload/project_file.py b/autoload/project_file.py new file mode 100644 index 0000000..0667694 --- /dev/null +++ b/autoload/project_file.py @@ -0,0 +1,98 @@ +import os +import shlex + +ANY_ARG = object() + +# [ ([match arg1, match arg2, ...], lambda matched_args: filtered_args) ] +# +# If the lambda is not given, it defaults to lambda l: [] +ARG_DEFS = [ + ( ["-h"], ), + ( ["-help"], ), + ( ["-no-opt"], ), + ( ["-byte"], ), + ( ["-full"], ), + ( ["-opt"], ), + ( ["-impredicative-set"], lambda l: ("-impredicative-set",) ), + ( ["-no-install"], ), + ( ["-install", ANY_ARG], ), + ( ["-custom", ANY_ARG, ANY_ARG, ANY_ARG], ), + ( ["-extra", ANY_ARG, ANY_ARG, ANY_ARG], ), + ( ["-extra-phony", ANY_ARG, ANY_ARG, ANY_ARG], ), + ( ["-Q", ANY_ARG, ANY_ARG], lambda l: l ), + ( ["-I", ANY_ARG], lambda l: l ), + ( ["-R", ANY_ARG, ANY_ARG], lambda l: l ), + ( ["-Q"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-R"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-I"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-custom"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-extra"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-extra-phony"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-f", ANY_ARG], lambda l: Exception(l[0] + " not supported") ), + ( ["-f"], lambda l: Exception(l[0] + " needs an argument") ), + ( ["-o", ANY_ARG], ), + ( [ANY_ARG, "=", ANY_ARG], ), + ( ["-arg", ANY_ARG], lambda l: (l[1],) ), + ( [ANY_ARG], ), + ] + +def parse_args(args): + "Filter the args from the project file down to those that go to coqtop" + result = [] + i = 0 + while i < len(args): + for d in ARG_DEFS: + match = True + j = 0 + while j < len(d[0]): + if i + j >= len(args): + match = False + break + if d[0][j] is ANY_ARG: + j += 1 + continue + if args[i + j] != d[0][j]: + match = False + break + j += 1 + if match: + if len(d) > 1: + filtered = d[1](args[i:i + j]) + if filtered is Exception: + raise filtered + else: + result.extend(filtered) + i += j + break + return result + +def parse_file(project_file): + "Parse coqtop args from _CoqProject" + with open(project_file, "r") as f: + project_args = shlex.split(f.read(), comments=True) + return parse_args(project_args) + +def find_file(source_file): + "Find the _CoqProject corresponding to a .v source file" + # Starting with the source buffer's directoy, walk up the tree until + # one of the directories has a _CoqProject file. + project_dir = os.path.dirname(source_file) + while project_dir is not None: + project_path = os.path.join(project_dir, "_CoqProject") + if os.path.isfile(project_path): + break + else: + project_path = None + parent = os.path.join(project_dir, os.pardir) + if os.path.samefile(parent, project_dir): + project_dir = None + else: + project_dir = parent + return project_path + +def find_and_parse_file(source_file): + project_file = find_file(source_file) + if project_file is not None: + return parse_file(project_file) + else: + return [] diff --git a/ftdetect/coq.vim b/ftdetect/coq.vim index e745ae9..e82537d 100644 --- a/ftdetect/coq.vim +++ b/ftdetect/coq.vim @@ -1 +1,3 @@ -au BufRead,BufNewFile *.v set filetype=coq +" Set the file type to coq for coq source files. For the supporting buffers, +" restore the file type after it gets overridden by other file type detectors. +au BufRead,BufNewFile *.v let &filetype = getbufvar("", "coquille_filetype", "coq") From 848e33e727608be35049856a76b357845cdb4952 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sun, 24 Sep 2017 00:24:22 -0700 Subject: [PATCH 04/12] Handle errors where coqtop reports it failed in state 0 If the error is serious enough, coqtop reports it happened in state 0. It is not possible to revert to state 0, because that is before the Init call. So skip the revert completely if coqtop says state 0. --- autoload/coqtop.py | 5 +++++ autoload/coquille.py | 15 ++++++++------- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index fedc818..bd1037a 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -463,6 +463,11 @@ def goals(self, feedback_callback): vp = self.call('Goal', (), feedback_callback=feedback_callback) if isinstance(vp, Ok): return vp + if vp.revert_state.id == 0: + if vp.err not in self.error_messages: + self.error_messages.append(vp.err) + # Can't revert to state 0 (which is before the Init) + return vp # An error occurred. Revert back to the state coqtop requested, and ask # for the goal again. revert_count = 0 diff --git a/autoload/coquille.py b/autoload/coquille.py index 8cd4fc6..ff9690a 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -264,10 +264,10 @@ def update(): # trigger it to start processing all the commands that have been added. # So show_goal needs to be called before waiting for all the unchecked # commands finished. - self.show_goal(update) - while self.coq_top.has_unchecked_commands(): - self.coq_top.process_response() - update() + if self.show_goal(update): + while self.coq_top.has_unchecked_commands(): + self.coq_top.process_response() + update() update() def show_goal(self, feedback_callback): @@ -282,14 +282,14 @@ def show_goal(self, feedback_callback): if response is None: vim.command("call coquille#KillSession()") print('ERROR: the Coq process died') - return + return False if isinstance(response, CT.Err): - return + return False if response.val.val is None: self.goal_buffer[0] = 'No goals.' - return + return True goals = response.val.val @@ -316,6 +316,7 @@ def show_goal(self, feedback_callback): self.goal_buffer.append('') finally: self.goal_buffer.options["modifiable"] = modifiable + return True def show_info(self, message): # Temporarily make the info buffer modifiable From a58f4e92f0f862e520b099a13dd40e24623687b9 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sun, 24 Sep 2017 14:09:56 -0700 Subject: [PATCH 05/12] Rewind the first time new text is inserted in the processed region The CursorMovedI event is triggered when new text is inserted, which is better than InsertEnter that would resync the buffer on the next insert. Also fix an off by one error around changing the last character in a statement, or jumping to the last character in a statement. --- autoload/coquille.py | 18 ++++++++++++++++-- autoload/coquille.vim | 18 ++++++++++-------- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/autoload/coquille.py b/autoload/coquille.py index ff9690a..b8b9e49 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -111,7 +111,8 @@ def sync(self): self._reset() else: (line, col) = self.saved_sync.pos() - self.rewind_to(line - 1, col) # vim indexes from lines 1, coquille from 0 + # vim indexes from lines 1, coquille from 0 + self.rewind_to(line - 1, col - 1) self.saved_sync = curr_sync def _reset(self): @@ -173,7 +174,9 @@ def coq_to_cursor(self): else self.coq_top.states[-1].end) if cline < line or (cline == line and ccol < col): - self.rewind_to(cline - 1, ccol) + # Add 1 to the column to leave whatever is at the + # cursor as sent. + self.rewind_to(cline - 1, ccol + 1) else: while True: r = self._get_message_range((line, col)) @@ -422,12 +425,23 @@ def reset_color(self): self.source_buffer.number) def rewind_to(self, line, col): + """ Go backwards to the specified position + + line and col are 0-based and point to the first position to + remove from the sent region. + """ if self.coq_top.coqtop is None: print('Internal error: vimbufsync is still being called but coqtop\ appears to be down.') print('Please report.') return + if self.coq_top.states and self.coq_top.states[-1].end <= (line, col): + # The caller asked to rewind to a position after what has been + # processed. This quick path exits without having to search the + # state list. + return + predicate = lambda x: x.end <= (line, col) lst = filter(predicate, self.coq_top.states) steps = len(self.coq_top.states) - len(list(lst)) diff --git a/autoload/coquille.vim b/autoload/coquille.vim index 68a8bc4..81307ed 100644 --- a/autoload/coquille.vim +++ b/autoload/coquille.vim @@ -213,14 +213,16 @@ function! coquille#OpenSupportingBuffers(bufid, ...) call setbufvar(a:bufid, "errors", -1) execute "autocmd BufUnload call coquille#DetachSupportingBuffers(". a:bufid .")" - " 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. - " It's still incomplete though, the plugin won't sync when you undo or - " delete some part of your buffer. So the highlighting will be wrong, but - " nothing really problematic will happen, as sync will be called the next - " time you explicitly call a command (be it 'rewind' or 'interp') - execute "autocmd InsertEnter call coquille#Python('" \ "coquille.BufferState.lookup_bufid(". \ a:bufid . ").sync()')" From c4e4b98090273a9966e37daf6aef92a924ad64eb Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sun, 24 Sep 2017 23:44:31 -0700 Subject: [PATCH 06/12] Fix bullet handling 1. Allow multi character bullets, like -- 2. Do not treat the space directly after the bullet as part of the bullet. This is important so that when a new statement is added directly after the bullet, the bullet is not rewound. --- autoload/coquille.py | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/autoload/coquille.py b/autoload/coquille.py index b8b9e49..0994b06 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -170,19 +170,20 @@ def coq_to_cursor(self): self.sync() (cline, ccol) = vim.current.window.cursor + cline -= 1 (line, col) = ((0,0) if not self.coq_top.states else self.coq_top.states[-1].end) if cline < line or (cline == line and ccol < col): # Add 1 to the column to leave whatever is at the # cursor as sent. - self.rewind_to(cline - 1, ccol + 1) + self.rewind_to(cline, ccol + 1) else: while True: r = self._get_message_range((line, col)) - if r is not None and r['stop'] <= (cline - 1, ccol): + if r is not None and r['stop'] <= (cline, ccol + 1): line = r['stop'][0] - col = r['stop'][1] + 1 + col = r['stop'][1] self.send_queue.append(r) else: break @@ -464,11 +465,12 @@ def send_until_fail(self): while len(self.send_queue) > 0: message_range = self.send_queue.popleft() - message = self._between(message_range['start'], message_range['stop']) - (eline, ecol) = message_range['stop'] + message = self._between(message_range['start'], + (eline, ecol - 1)) + response = self.coq_top.advance(message, - (eline, ecol + 1), encoding) + (eline, ecol), encoding) if response is None: vim.command("call coquille#KillSession()") @@ -520,6 +522,14 @@ def _get_message_range(self, after): end_pos = self._find_next_chunk(line, col) return { 'start':after , 'stop':end_pos } if end_pos is not None else None + # A bullet is: + # - One or more '-' + # - One or more '+' + # - One or more '*' + # - Exactly 1 '{' (additional ones are parsed as separate statements) + # - Exactly 1 '}' (additional ones are parsed as separate statements) + bullets = re.compile("-+|\++|\*+|{|}") + def _find_next_chunk(self, line, col): """ Returns the position of the next chunk dot after a certain position. @@ -527,7 +537,6 @@ def _find_next_chunk(self, line, col): by a dot (outside of a comment, and not denoting a path). """ blen = len(self.source_buffer) - bullets = ['{', '}', '-', '+', '*'] # We start by striping all whitespaces (including \n) from the beginning of # the chunk. while line < blen and self.source_buffer[line][col:].strip() == '': @@ -546,8 +555,9 @@ def _find_next_chunk(self, line, col): # might not have been sent/detected yet). # 2/ The bullet chars can never be used at the *beginning* of a chunk # outside of a proof. So the check was unecessary. - if self.source_buffer[line][col] in bullets: - return (line, col + 1) + bullet_match = self.bullets.match(self.source_buffer[line], col) + if bullet_match: + return (line, bullet_match.end()) # We might have a commentary before the bullet, we should be skiping it and # keep on looking. @@ -561,7 +571,12 @@ def _find_next_chunk(self, line, col): # If the chunk doesn't start with a bullet, we look for a dot. - return self._find_dot_after(line, col) + dot = self._find_dot_after(line, col) + if dot: + # Return the position one after the dot + return (dot[0], dot[1] + 1) + else: + return None def _find_dot_after(self, line, col): """ From ff530795a5f571c1cc2195b0d6d51bd1e5ebc435 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sat, 30 Sep 2017 09:19:45 -0700 Subject: [PATCH 07/12] Fix highlight ranges for files with non-ascii characters Use byte offsets for the highlight ranges (sent, checked, error, and warning) instead of unicode characters offsets. Also fix python 2 support. --- autoload/coqtop.py | 18 ++++-- autoload/coquille.py | 143 +++++++++++++++++++++++++++++-------------- 2 files changed, 109 insertions(+), 52 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index bd1037a..54a04d1 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -12,7 +12,10 @@ from collections import deque, namedtuple # Define unicode in python 3 -unicode = getattr(__builtins__, 'unicode', str) +if isinstance(__builtins__, dict): + unicode = __builtins__.get('unicode', str) +else: + unicode = getattr(__builtins__, 'unicode', str) Ok = namedtuple('Ok', ['val', 'msg']) Err = namedtuple('Err', ['err', 'revert_state', 'loc_s', 'loc_e']) @@ -166,10 +169,14 @@ def ignore_sigint(): signal.signal(signal.SIGINT, signal.SIG_IGN) def escape(cmd): - return cmd.replace(" ", ' ') \ + escaped = cmd.replace(" ", ' ') \ .replace("'", '\'') \ .replace("(", '(') \ .replace(")", ')') + if isinstance(escaped, str): + return escaped + else: + return escaped.encode('ascii', 'xmlcharrefreplace') class Command(object): # Command was sent to coqtop through an Add call, and coq acknowledged the @@ -194,9 +201,10 @@ def __init__(self, end): Command.next_edit -= 1 self.state_id = None self.state = self.SENT - # A (line, col) pair. Both the line and col are 0-indexed. The end + # A (line, col, byte) pair. line, col, and byte are 0-indexed. The end # position is one column after the last character included in the # command. + assert(len(end) == 3) self.end = end # A byte offset relative to the start of this command where the warning # or error starts. @@ -315,7 +323,7 @@ def parse_message(self, xml): def process_response(self): fd = self.coqtop.stdout.fileno() - data = '' + data = u'' while True: try: data += os.read(fd, 0x4000).decode("utf-8") @@ -402,7 +410,7 @@ def restart_coq(self, *args): r = self.call('Init', Option(None)) assert isinstance(r, Ok) - comm = Command((0, 0)) + comm = Command((0, 0, 0)) comm.edit_id = None comm.state_id = r.val comm.state = Command.PROCESSED diff --git a/autoload/coquille.py b/autoload/coquille.py index 0994b06..feb0981 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -16,7 +16,10 @@ vimbufsync.check_version([0,1,0], who="coquille") # Define unicode in python 3 -unicode = getattr(__builtins__, 'unicode', str) +if isinstance(__builtins__, dict): + unicode = __builtins__.get('unicode', str) +else: + unicode = getattr(__builtins__, 'unicode', str) # Cache whether vim has a bool type vim_has_bool = vim.eval("exists('v:false')") @@ -42,9 +45,10 @@ def vim_repr(value): return value.replace("'", "''") return "unknown" -# Convert 0-based (line, col) pairs into 1-based lists +# Convert 0-based (line, col, byte) tuples into 1-based lists in the form +# [line, byte] def make_vim_range(start, stop): - return [[start[0] + 1, start[1] + 1], [stop[0] + 1, stop[1] + 1]] + return [[start[0] + 1, start[2] + 1], [stop[0] + 1, stop[2] + 1]] # All the python side state associated with the vim source buffer class BufferState(object): @@ -171,8 +175,9 @@ def coq_to_cursor(self): (cline, ccol) = vim.current.window.cursor cline -= 1 - (line, col) = ((0,0) if not self.coq_top.states - else self.coq_top.states[-1].end) + last_sent = ((0,0,0) if not self.coq_top.states + else self.coq_top.states[-1].end) + (line, col, byte) = last_sent if cline < line or (cline == line and ccol < col): # Add 1 to the column to leave whatever is at the @@ -180,10 +185,10 @@ def coq_to_cursor(self): self.rewind_to(cline, ccol + 1) else: while True: - r = self._get_message_range((line, col)) - if r is not None and r['stop'] <= (cline, ccol + 1): - line = r['stop'][0] - col = r['stop'][1] + r = self._get_message_range(last_sent) + if (r is not None + and (r['stop'][0], r['stop'][1]) <= (cline, ccol + 1)): + last_sent = r['stop'] self.send_queue.append(r) else: break @@ -197,12 +202,13 @@ def coq_next(self): self.sync() - (line, col) = ((0,0) if not self.coq_top.states - else self.coq_top.states[-1].end) - message_range = self._get_message_range((line, col)) + last_sent = ((0,0,0) if not self.coq_top.states + else self.coq_top.states[-1].end) + message_range = self._get_message_range(last_sent) if message_range is None: return + assert(len(message_range['start']) == 3) self.send_queue.append(message_range) self.send_until_fail() @@ -255,15 +261,14 @@ def debug(self): ##################################### def refresh(self): - last_info = None + last_info = [None] def update(): - nonlocal last_info self.reset_color() vim.command('redraw') new_info = self.coq_top.get_errors() - if last_info != new_info: + if last_info[0] != new_info: self.show_info(new_info) - last_info = new_info + last_info[0] = new_info # It seems that coqtop needs some kind of call like Status or Goal to # trigger it to start processing all the commands that have been added. # So show_goal needs to be called before waiting for all the unchecked @@ -353,8 +358,9 @@ def clear_info(self): def convert_offset(self, range_start, offset, range_end): message = self._between(range_start, range_end) - (line, col) = _pos_from_offset(range_start[1], message, offset) - return (line + range_start[0], col) + (line, col, byte) = _pos_from_offset(range_start[1], range_start[2], + message, offset) + return (line + range_start[0], col, byte) def reset_color(self): sent = [] @@ -437,13 +443,15 @@ def rewind_to(self, line, col): print('Please report.') return - if self.coq_top.states and self.coq_top.states[-1].end <= (line, col): + if (self.coq_top.states and + (self.coq_top.states[-1].end[0], + self.coq_top.states[-1].end[1]) <= (line, col)): # The caller asked to rewind to a position after what has been # processed. This quick path exits without having to search the # state list. return - predicate = lambda x: x.end <= (line, col) + predicate = lambda x: (x.end[0], x.end[1]) <= (line, col) lst = filter(predicate, self.coq_top.states) steps = len(self.coq_top.states) - len(list(lst)) if steps != 0: @@ -465,12 +473,12 @@ def send_until_fail(self): while len(self.send_queue) > 0: message_range = self.send_queue.popleft() - (eline, ecol) = message_range['stop'] + (eline, ecol, ebyte) = message_range['stop'] message = self._between(message_range['start'], - (eline, ecol - 1)) + (eline, ecol - 1, ebyte - 1)) response = self.coq_top.advance(message, - (eline, ecol), encoding) + (eline, ecol, ebyte), encoding) if response is None: vim.command("call coquille#KillSession()") @@ -485,10 +493,15 @@ def send_until_fail(self): loc_s = response.loc_s if loc_s is not None: loc_e = response.loc_e - (l, c) = message_range['start'] - (l_start, c_start) = _pos_from_offset(c, message, loc_s) - (l_stop, c_stop) = _pos_from_offset(c, message, loc_e) - self.error_at = ((l + l_start, c_start), (l + l_stop, c_stop)) + (l, c, b) = message_range['start'] + (l_start, c_start, b_start) = _pos_from_offset(c, b, + message, + loc_s) + (l_stop, c_stop, b_stop) = _pos_from_offset(c, b, + message, + loc_e) + self.error_at = ((l + l_start, c_start, b_start), + (l + l_stop, c_stop, b_stop)) else: print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) break @@ -502,25 +515,50 @@ def send_until_fail(self): # Miscellaneous # ################# + # col_offset is a character offset, not byte offset + def _get_remaining_line(self, line, col_offset): + s = self.source_buffer[line] + if not isinstance(s, unicode): + s = s.decode("utf-8") + return s[col_offset:] + def _between(self, begin, end): """ Returns a string corresponding to the portion of the buffer between the [begin] and [end] positions. """ - (bline, bcol) = begin - (eline, ecol) = end + (bline, bcol, bbyte) = begin + (eline, ecol, ebyte) = end acc = "" for line, str in enumerate(self.source_buffer[bline:eline + 1]): + if not isinstance(str, unicode): + str = str.decode("utf-8") start = bcol if line == 0 else 0 stop = ecol + 1 if line == eline - bline else len(str) acc += str[start:stop] + '\n' return acc + # Convert a pos from (line, col) to (line, col, byte_offset) + # + # The byte_offset is relative to the start of the line. It is the same as + # col, unless there are non-ascii characters. + # + # line, col, and byte_offset are all 0-indexed. + def _add_byte_offset(self, pos): + (line, col) = pos + s = self.source_buffer[line] + if not isinstance(s, unicode): + s = s.decode("utf-8") + return (line, col, len(s[:col].encode("utf-8"))) + def _get_message_range(self, after): """ See [_find_next_chunk] """ - (line, col) = after + (line, col, byte) = after end_pos = self._find_next_chunk(line, col) - return { 'start':after , 'stop':end_pos } if end_pos is not None else None + if end_pos is None: + return None + else: + return { 'start':after , 'stop':self._add_byte_offset(end_pos) } # A bullet is: # - One or more '-' @@ -539,15 +577,19 @@ def _find_next_chunk(self, line, col): blen = len(self.source_buffer) # We start by striping all whitespaces (including \n) from the beginning of # the chunk. - while line < blen and self.source_buffer[line][col:].strip() == '': + while line < blen: + line_val = self.source_buffer[line] + if not isinstance(line_val, unicode): + line_val = line_val.decode("utf-8") + while col < len(line_val) and line_val[col] in (' ', '\t'): + col += 1 + if col < len(line_val) and line_val[col] not in (' ', '\t'): + break line += 1 col = 0 if line >= blen: return - while self.source_buffer[line][col] == ' ': # FIXME: keeping the stripped line would be - col += 1 # more efficient. - # Then we check if the first character of the chunk is a bullet. # Intially I did that only when I was sure to be in a proof (by looking in # [encountered_dots] whether I was after a "collapsable" chunk or not), but @@ -555,15 +597,15 @@ def _find_next_chunk(self, line, col): # might not have been sent/detected yet). # 2/ The bullet chars can never be used at the *beginning* of a chunk # outside of a proof. So the check was unecessary. - bullet_match = self.bullets.match(self.source_buffer[line], col) + bullet_match = self.bullets.match(line_val, col) if bullet_match: return (line, bullet_match.end()) # We might have a commentary before the bullet, we should be skiping it and # keep on looking. - tail_len = len(self.source_buffer[line]) - col - if ((tail_len - 1 > 0) and self.source_buffer[line][col] == '(' - and self.source_buffer[line][col + 1] == '*'): + tail_len = len(line_val) - col + if ((tail_len - 1 > 0) and line_val[col] == '(' + and line_val[col + 1] == '*'): com_end = self._skip_comment(line, col + 2, 1) if not com_end: return (line, col) = com_end @@ -585,7 +627,7 @@ def _find_dot_after(self, line, col): comments, strings or ident paths are not valid. """ if line >= len(self.source_buffer): return - s = self.source_buffer[line][col:] + s = self._get_remaining_line(line, col) dot_pos = s.find('.') com_pos = s.find('(*') str_pos = s.find('"') @@ -610,10 +652,10 @@ def _find_dot_after(self, line, col): # just after the module name. # Example: [Require Import Coq.Arith] return self._find_dot_after(line, col + dot_pos + 1) - elif dot_pos + col > 0 and self.source_buffer[line][col + dot_pos - 1] == '.': + elif dot_pos + col > 0 and self._get_remaining_line(line, col + dot_pos - 1)[0] == '.': # FIXME? There might be a cleaner way to express this. # We don't want to capture ".." - if dot_pos + col > 1 and self.source_buffer[line][col + dot_pos - 2] == '.': + if dot_pos + col > 1 and self._get_remaining_line(line, col + dot_pos - 2)[0] == '.': # But we want to capture "..." return (line, dot_pos + col) else: @@ -630,7 +672,7 @@ def _skip_str(self, line, col): """ while True: if line >= len(self.source_buffer): return - s = self.source_buffer[line][col:] + s = self._get_remaining_line(line, col) str_end = s.find('"') if str_end > -1: return (line, col + str_end + 1) @@ -645,7 +687,7 @@ def _skip_comment(self, line, col, nb_left): """ while nb_left > 0: if line >= len(self.source_buffer): return None - s = self.source_buffer[line][col:] + s = self._get_remaining_line(line, col) com_start = s.find('(*') com_end = s.find('*)') if com_end > -1 and (com_end < com_start or com_start == -1): @@ -662,9 +704,16 @@ def _skip_comment(self, line, col, nb_left): def _empty_range(): return [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] -def _pos_from_offset(col, msg, offset): - str = msg[:offset] +# Converts a byte offset into a message into a (line, col, byte) tuple +# +# msg is a unicode string the offset is relative to. col is the column where +# msg starts, and byte is the byte offset where it starts. +# +# All indecies are 0 based. +def _pos_from_offset(col, byte, msg, offset): + str = msg.encode("utf-8")[:offset].decode("utf-8") lst = str.split('\n') line = len(lst) - 1 col = len(lst[-1]) + (col if line == 0 else 0) - return (line, col) + byte = len(lst[-1].encode("utf-8")) + (byte if line == 0 else 0) + return (line, col, byte) From 49f338222ba9a554072d1df90602e511faf3c6cf Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Mon, 2 Oct 2017 23:22:12 -0700 Subject: [PATCH 08/12] If there are no focused goals, print the unfocused goals Match the coqide's goal message format. This is important for indicating whether an unfocused goal needs to be focused or the proof is done. --- autoload/coquille.py | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/autoload/coquille.py b/autoload/coquille.py index feb0981..14eb618 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -303,21 +303,36 @@ def show_goal(self, feedback_callback): goals = response.val.val sub_goals = goals.fg + msg_format = '{0} subgoal{1}' + show_hyps = True + if not sub_goals: + show_hyps = False + sub_goals = [] + for (before, after) in goals.bg: + sub_goals.extend(reversed(before)) + sub_goals.extend(after) + if sub_goals: + msg_format = ('This subproof is complete, but there {2} {0}' + ' unfocused goal{1}') + if not sub_goals: + msg_format = 'No more subgoals.' nb_subgoals = len(sub_goals) - plural_opt = '' if nb_subgoals == 1 else 's' - self.goal_buffer[0] = '%d subgoal%s' % (nb_subgoals, plural_opt) + self.goal_buffer[0] = msg_format.format(nb_subgoals, + '' if nb_subgoals == 1 else 's', + 'is' if nb_subgoals == 1 else 'are') self.goal_buffer.append(['']) for idx, sub_goal in enumerate(sub_goals): _id = sub_goal.id hyps = sub_goal.hyp ccl = sub_goal.ccl - if idx == 0: + if show_hyps: # we print the environment only for the current subgoal for hyp in hyps: lst = map(lambda s: s.encode('utf-8'), hyp.split('\n')) self.goal_buffer.append(list(lst)) + show_hyps = False self.goal_buffer.append('') self.goal_buffer.append('======================== ( %d / %d )' % (idx+1 , nb_subgoals)) lines = map(lambda s: s.encode('utf-8'), ccl.split('\n')) From 177540eec128d7b5db95d309523a2e9263dd2c1a Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sat, 14 Oct 2017 23:17:11 -0700 Subject: [PATCH 09/12] Send Coq statements on a background thread For the coq to cursor command, send the statements on a background thread while the main thread redraws the screen. This lets Coq accept multiple commands per screen redraw. The background thread is terminated after all the statements are sent. --- autoload/coqtop.py | 399 +++++++++++++++++++++++++++++-------------- autoload/coquille.py | 174 ++++++++----------- 2 files changed, 335 insertions(+), 238 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 54a04d1..e255440 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -8,6 +8,7 @@ import xml.etree.ElementTree as ET import signal import sys +import threading from collections import deque, namedtuple @@ -179,20 +180,29 @@ def escape(cmd): return escaped.encode('ascii', 'xmlcharrefreplace') class Command(object): + # Values for self.state + # ---------------------- # Command was sent to coqtop through an Add call, and coq acknowledged the # Add. SENT = 0 - # The worker that was processing this command died before finishing - # processing the command. The command will never be finished. + # Either the worker that was processing this command died before finishing + # processing the command, or coq rejected the Add call. The command will + # never be finished. ABANDONED = 1 # coqtop marked the command as processed through a feedback statement. PROCESSED = 2 + REVERTED = 3 + + # Values for self.msg_type + # ---------------------------- + # + NONE = 0 # coqtop sent a warning level message for the command through a feedback # statement. - WARNING = 3 + WARNING = 1 # coqtop sent an error level message for the command through a feedback # statement. - ERROR = 4 + ERROR = 2 next_edit = -1 @@ -206,6 +216,7 @@ def __init__(self, end): # command. assert(len(end) == 3) self.end = end + self.msg_type = self.NONE # A byte offset relative to the start of this command where the warning # or error starts. self.msg_start_offset = None @@ -220,6 +231,11 @@ def __init__(self, end): self.worker = None class CoqTop(object): + # bit fields for self.result + COMMAND_CHANGED = 1 + MESSAGE_RECEIVED = 2 + SEND_DONE = 4 + def __init__(self): self.coqtop = None self.states = [] @@ -228,21 +244,27 @@ def __init__(self): # reverted commands. This is important because sometimes coqtop forces # the state to get reverted. # the states to get reverted. - self.reverted_states = [] - self.error_messages = [] + self.messages = [] - def kill_coqtop(self): - if self.coqtop: - try: - self.coqtop.terminate() - self.coqtop.communicate() - except OSError: - pass - self.coqtop = None - self.states = [] - self.clear_errors() + self.lock = threading.Lock() + self.result = 0 + self.has_result = threading.Condition(self.lock) + self.send_thread = None - def get_command(self, state_id): + def kill_coqtop(self): + with self.lock: + if self.coqtop: + try: + self.coqtop.terminate() + self.coqtop.communicate() + except OSError: + pass + self.coqtop = None + self.states = [] + self.reverted_index = 0 + self.messages = [] + + def get_command_by_state_id(self, state_id): for s in self.states: if s.state_id == state_id: return s @@ -254,12 +276,37 @@ def get_command_by_edit(self, edit_id): return s return None + def check_state_indexes(self): + assert self.reverted_index <= len(self.states) + + def get_active_command_count(self): + with self.lock: + self.check_state_indexes() + return self.reverted_index + + def get_last_active_command(self): + with self.lock: + self.check_state_indexes() + if self.reverted_index > 0: + return self.states[self.reverted_index - 1] + else: + return None + + def get_active_commands(self): + with self.lock: + self.check_state_indexes() + return list(self.states[0:self.reverted_index]) + + def get_commands(self): + with self.lock: + return list(self.states) + def parse_feedback(self, xml): assert xml.tag == 'feedback' message = None if xml.get("object") == "state": state_id = parse_value(xml.find("state_id")) - comm = self.get_command(state_id) + comm = self.get_command_by_state_id(state_id) else: edit_id = parse_value(xml.find("edit_id")) comm = self.get_command_by_edit(edit_id) @@ -274,14 +321,20 @@ def parse_feedback(self, xml): else: level = Command.WARNING if comm: - comm.state = level + comm.msg_type = level # The element type is option if messageNode[1].get("val") == "some": loc = messageNode[1].find("loc") comm.msg_start_offset = int(loc.get("start")) comm.msg_stop_offset = int(loc.get("stop")) + # Only transition from SENT to PROCESSED. + if comm.state == Command.SENT: + comm.state = Command.PROCESSED + self.result |= self.COMMAND_CHANGED message = parse_value(messageNode.find("richpp")) - self.error_messages.append(message) + self.messages.append(message) + self.result |= self.MESSAGE_RECEIVED + self.has_result.notify() elif feedback_type == "processingin": if comm is not None: comm.worker = parse_value(feedback_content[0]) @@ -290,22 +343,17 @@ def parse_feedback(self, xml): if status == "Dead": # The worker died. Mark all commands it was processing as # abandoned. - for c in self.states: + for c in self.states[0:self.reverted_index]: if c.state == Command.SENT and c.worker == worker: c.state = Command.ABANDONED + self.result |= self.COMMAND_CHANGED + self.has_result.notify() elif feedback_type == "processed": - # Only transition from SENT to PROCESSED. coqtop likes to send out - # extra feedback messages. Do not let it transition the command - # from WARNING to PROCESSED. - # - # Also note that sometimes coqtop sends processed feedback for - # commands that it hasn't sent the Add reply for yet. Its difficult - # to process the feedback when the correspondance between the - # Command and state_id isn't known yet. So that feedback can be - # ignored. coqtop will send another processed feedback after the - # Add reply is sent. + # Only transition from SENT to PROCESSED. if comm and comm.state == Command.SENT: comm.state = Command.PROCESSED + self.result |= self.COMMAND_CHANGED + self.has_result.notify() return message def parse_message(self, xml): @@ -313,13 +361,14 @@ def parse_message(self, xml): level = xml.find('message_level') if level is not None: level = level.get('val') - if level == 'warning' and self.states: - comm = self.states[-1] + self.check_state_indexes() + if level == 'warning' and self.reverted_index > 0: + comm = self.states[self.reverted_index - 1] if comm.state_id is None: # Attach the warning message to the command that is currently being # parsed. - comm.state = Command.WARNING - self.error_messages.append(parse_value(xml[2])) + comm.msg_type = Command.WARNING + self.messages.append(parse_value(xml[2])) def process_response(self): fd = self.coqtop.stdout.fileno() @@ -329,32 +378,33 @@ def process_response(self): data += os.read(fd, 0x4000).decode("utf-8") try: elt = ET.fromstring('' + escape(data) + '') - # The data parsed correctly. Clear it so that it isn't - # parsed again when new data comes in. - data = '' - valueNode = None - messageNode = None - for c in elt: - if c.tag == 'value': - valueNode = c - if c.tag == 'message': - self.parse_message(c) - # Extract messages from feedbacks to handle errors - if c.tag == 'feedback': - messageNode = self.parse_feedback(c) - if valueNode is None: - return None - vp = parse_response(valueNode) - if messageNode is not None: - if isinstance(vp, Ok): - return Ok(vp.val, messageNode) - elif isinstance(vp, Err): - if vp.err not in self.error_messages: - self.error_messages.append(vp.err) - # Override error message : coq provides one - return Err(messageNode, vp.revert_state, - vp.loc_s, vp.loc_e) - return vp + with self.lock: + # The data parsed correctly. Clear it so that it isn't + # parsed again when new data comes in. + data = '' + valueNode = None + messageNode = None + for c in elt: + if c.tag == 'value': + valueNode = c + if c.tag == 'message': + self.parse_message(c) + # Extract messages from feedbacks to handle errors + if c.tag == 'feedback': + messageNode = self.parse_feedback(c) + if valueNode is None: + return None + vp = parse_response(valueNode) + if messageNode is not None: + if isinstance(vp, Ok): + return Ok(vp.val, messageNode) + elif isinstance(vp, Err): + if vp.err not in self.messages: + self.messages.append(vp.err) + # Override error message : coq provides one + return Err(messageNode, vp.revert_state, + vp.loc_s, vp.loc_e) + return vp except ET.ParseError: continue except OSError: @@ -372,9 +422,9 @@ def get_answer(self, feedback_callback): if feedback_callback is not None: feedback_callback() - def call(self, name, arg, encoding='utf-8', feedback_callback=None): + def call(self, name, arg, feedback_callback=None): xml = encode_call(name, arg) - msg = ET.tostring(xml, encoding) + msg = ET.tostring(xml, 'utf-8') self.send_cmd(msg) response = self.get_answer(feedback_callback) return response @@ -393,29 +443,33 @@ def restart_coq(self, *args): , 'on' ] try: - if os.name == 'nt': - self.coqtop = subprocess.Popen( - options + list(args) - , stdin = subprocess.PIPE - , stdout = subprocess.PIPE - , stderr = subprocess.STDOUT - ) - else: - self.coqtop = subprocess.Popen( - options + list(args) - , stdin = subprocess.PIPE - , stdout = subprocess.PIPE - , preexec_fn = ignore_sigint - ) + with self.lock: + if os.name == 'nt': + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , stderr = subprocess.STDOUT + ) + else: + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , preexec_fn = ignore_sigint + ) r = self.call('Init', Option(None)) - assert isinstance(r, Ok) - comm = Command((0, 0, 0)) - comm.edit_id = None - comm.state_id = r.val - comm.state = Command.PROCESSED - self.states = [comm] - return True + with self.lock: + assert isinstance(r, Ok) + comm = Command((0, 0, 0)) + comm.edit_id = None + comm.state_id = r.val + comm.state = Command.PROCESSED + self.states = [comm] + self.reverted_index = len(self.states) + self.check_state_indexes() + return True except OSError as e: print("Error: couldn't launch coqtop:", e) return False @@ -424,66 +478,147 @@ def launch_coq(self, *args): return self.restart_coq(*args) def cur_state(self): - return self.states[-1].state_id + self.check_state_indexes() + return self.states[self.reverted_index - 1].state_id - # Clear the error messages from old commands. + # Clear the messages from old commands. # # The error state and location of non-reverted commands will stay, but # their error messages will be reverted. - def clear_errors(self): - self.reverted_states = [] - self.error_messages = [] - - def get_errors(self): - return "\n".join(self.error_messages) - - def advance(self, cmd, end, encoding = 'utf-8'): - cur_state = self.cur_state() - comm = Command(end) - self.states.append(comm) + def clear_messages(self): + with self.lock: + self.check_state_indexes() + self.messages = [] + del self.states[self.reverted_index:] + self.check_state_indexes() + + def get_messages(self): + with self.lock: + return "\n".join(self.messages) + + def advance(self, cmd, end): + with self.lock: + cur_state = self.cur_state() + assert self.reverted_index == len(self.states) + comm = Command(end) + self.states.append(comm) + self.reverted_index += 1 r = self.call('Add', ((cmd, comm.edit_id.id), - (cur_state, True)), encoding) - if r is None or isinstance(r, Err): - self.states = self.states[:len(self.states)-1] - self.reverted_states = [comm] + self.reverted_states + (cur_state, True))) + with self.lock: + if r is None or isinstance(r, Err): + comm.state = Command.ABANDONED + if r is not None: + self.messages.append(r.err) + comm.msg_start_offset = int(r.loc_s) + comm.msg_stop_offset = int(r.loc_e) + comm.msg_type = Command.ERROR + self.reverted_index -= 1 + return r + comm.state_id = r.val[0] return r - comm.state_id = r.val[0] - return r def rewind(self, step = 1, keep_states = False): - assert step <= len(self.states) - # At least one state, the root state, has to remain - assert step < len(self.states) - idx = len(self.states) - step - if keep_states: - self.reverted_states = self.states[idx:] + self.reverted_states - self.states = self.states[0:idx] - return self.call('Edit_at', self.cur_state()) - - def query(self, cmd, encoding = 'utf-8'): - r = self.call('Query', (cmd, self.cur_state()), encoding) + with self.lock: + # At least one state, the root state, has to remain + assert step < self.reverted_index + self.check_state_indexes() + idx = self.reverted_index - step + for c in self.states[idx:]: + c.state = Command.REVERTED + self.reverted_index = idx + if not keep_states: + del self.states[self.reverted_index:] + self.check_state_indexes() + rewind_state = self.cur_state() + return self.call('Edit_at', rewind_state) + + def query(self, cmd): + with self.lock: + cur_state = self.cur_state() + r = self.call('Query', (cmd, cur_state)) return r def has_unchecked_commands(self): - return any(c.state == Command.SENT for c in self.states) + with self.lock: + return any(c.state == Command.SENT for c in self.states[0:self.reverted_index]) def goals(self, feedback_callback): vp = self.call('Goal', (), feedback_callback=feedback_callback) if isinstance(vp, Ok): - return vp - if vp.revert_state.id == 0: - if vp.err not in self.error_messages: - self.error_messages.append(vp.err) - # Can't revert to state 0 (which is before the Init) - return vp - # An error occurred. Revert back to the state coqtop requested, and ask - # for the goal again. - revert_count = 0 - while (revert_count < len(self.states) and - self.states[-1 - revert_count].state_id.id > vp.revert_state.id): - revert_count += 1 - self.rewind(revert_count, keep_states = True) - return self.call('Goal', (), feedback_callback=feedback_callback) - - def read_states(self): - return self.states + return vp.val + with self.lock: + if vp.revert_state.id == 0: + if vp.err not in self.messages: + self.messages.append(vp.err) + # Can't revert to state 0 (which is before the Init). So revert + # back to the end of the contiguously processed section. + revert_to = 1 + while (revert_to + 1 < self.reverted_index and + self.states[revert_to + 1].state & Command.PROCESSED): + revert_to += 1 + else: + # An error occurred. Revert back to the state coqtop requested, and ask + # for the goal again. + revert_to = self.reverted_index + while (1 < revert_to and + self.states[revert_to - 1].state_id.id > vp.revert_state.id): + revert_to -= 1 + self.rewind(self.reverted_index - revert_to, keep_states = True) + vp = self.call('Goal', (), feedback_callback=feedback_callback) + if isinstance(vp, Ok): + return vp.val + else: + if vp.err not in self.messages: + self.messages.append(vp.err) + return None + + def send_async(self, send_queue): + """ + Tries to send every message in [send_queue] to Coq, stops at the first + error. + """ + assert self.send_thread == None + def process_queue(): + try: + for (message, end) in send_queue: + response = self.advance(message, end) + with self.lock: + self.result |= self.COMMAND_CHANGED + self.has_result.notify() + + if response is None: + self.messages.append('ERROR: the Coq process died') + self.result |= self.MESSAGE_RECEIVED + self.has_result.notify() + return + + if not isinstance(response, Ok): + if not isinstance(response, Err): + self.messages.append( + "(ANOMALY) unknown answer: %s" % + ET.tostring(response)) + self.result |= self.MESSAGE_RECEIVED + self.has_result.notify() + break + finally: + with self.lock: + self.result |= self.SEND_DONE + self.has_result.notify() + + self.send_thread = threading.Thread(target=process_queue, name="send thread") + self.send_thread.start() + + def wait_for_result(self): + with self.lock: + while self.result == 0: + self.has_result.wait() + result = self.result + self.result = 0 + return result + + def finish_send(self): + with self.lock: + thread = self.send_thread + self.send_thread = None + thread.join() diff --git a/autoload/coquille.py b/autoload/coquille.py index 14eb618..6c1493e 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -4,7 +4,6 @@ import vim -import itertools import re import xml.etree.ElementTree as ET import coqtop as CT @@ -77,13 +76,6 @@ def __init__(self, source_buffer): self.goal_buffer = None #: See vimbufsync ( https://github.com/def-lkb/vimbufsync ) self.saved_sync = None - - #: Keeps track of what have been checked by Coq, and what is waiting to be - #: checked. - self.send_queue = deque([]) - - self.error_at = None - self.coq_top = CT.CoqTop() def sync_vars(self): @@ -111,7 +103,7 @@ def sync_vars(self): def sync(self): curr_sync = vimbufsync.sync(self.source_buffer) if not self.saved_sync or curr_sync.buf() != self.saved_sync.buf(): - if len(self.coq_top.states) > 1: + if self.coq_top.get_active_command_count() > 1: self._reset() else: (line, col) = self.saved_sync.pos() @@ -121,9 +113,7 @@ def sync(self): def _reset(self): self.coq_top.kill_coqtop() - self.send_queue = deque([]) self.saved_sync = None - self.error_at = None self.reset_color() ##################### @@ -136,15 +126,15 @@ def kill_coqtop(self): self._reset() def goto_last_sent_dot(self): - (line, col) = ((0,1) if not self.coq_top.states - else self.coq_top.states[-1].end) + last = self.coq_top.get_last_active_command() + (line, col) = ((0,1) if not last else last.end) vim.current.window.cursor = (line + 1, col) def coq_rewind(self, steps=1): self.clear_info() # Do not allow the root state to be rewound - if steps < 1 or len(self.coq_top.states) < 2: + if steps < 1 or self.coq_top.get_active_command_count() < 2: return if self.coq_top.coqtop is None: @@ -175,8 +165,8 @@ def coq_to_cursor(self): (cline, ccol) = vim.current.window.cursor cline -= 1 - last_sent = ((0,0,0) if not self.coq_top.states - else self.coq_top.states[-1].end) + last = self.coq_top.get_last_active_command() + last_sent = ((0,0,0) if not last else last.end) (line, col, byte) = last_sent if cline < line or (cline == line and ccol < col): @@ -184,16 +174,17 @@ def coq_to_cursor(self): # cursor as sent. self.rewind_to(cline, ccol + 1) else: + send_queue = deque([]) while True: r = self._get_message_range(last_sent) if (r is not None - and (r['stop'][0], r['stop'][1]) <= (cline, ccol + 1)): - last_sent = r['stop'] - self.send_queue.append(r) + and (r[1][0], r[1][1]) <= (cline, ccol + 1)): + last_sent = r[1] + send_queue.append(r) else: break - self.send_until_fail() + self.send_until_fail(send_queue) def coq_next(self): if self.coq_top.coqtop is None: @@ -202,16 +193,16 @@ def coq_next(self): self.sync() - last_sent = ((0,0,0) if not self.coq_top.states - else self.coq_top.states[-1].end) + last = self.coq_top.get_last_active_command() + last_sent = ((0,0,0) if not last else last.end) message_range = self._get_message_range(last_sent) if message_range is None: return - assert(len(message_range['start']) == 3) - self.send_queue.append(message_range) + send_queue = deque([]) + send_queue.append(message_range) - self.send_until_fail() + self.send_until_fail(send_queue) if (vim.eval('g:coquille_auto_move') == 'true'): self.goto_last_sent_dot() @@ -225,16 +216,14 @@ def coq_raw_query(self, *args): raw_query = ' '.join(args) - encoding = vim.eval("&encoding") or 'utf-8' - - response = self.coq_top.query(raw_query, encoding) + response = self.coq_top.query(raw_query) if response is None: vim.command("call coquille#KillSession()") print('ERROR: the Coq process died') return - info_msg = self.coq_top.get_errors() + info_msg = self.coq_top.get_messages() self.show_info(info_msg) @@ -250,11 +239,11 @@ def launch_coq(self, *args): return self.coq_top.restart_coq(*args) def debug(self): - if self.coq_top.states: - print("encountered dots = [") - for (line, col) in self.coq_top.states: - print(" (%d, %d) ; " % (line, col)) - print("]") + commands = self.coq_top.get_active_commands() + print("encountered dots = [") + for (line, col) in commands: + print(" (%d, %d) ; " % (line, col)) + print("]") ##################################### # IDE tools: Goal, Infos and colors # @@ -265,7 +254,7 @@ def refresh(self): def update(): self.reset_color() vim.command('redraw') - new_info = self.coq_top.get_errors() + new_info = self.coq_top.get_messages() if last_info[0] != new_info: self.show_info(new_info) last_info[0] = new_info @@ -273,35 +262,28 @@ def update(): # trigger it to start processing all the commands that have been added. # So show_goal needs to be called before waiting for all the unchecked # commands finished. - if self.show_goal(update): + response = self.coq_top.goals(update) + if self.show_goal(response): while self.coq_top.has_unchecked_commands(): self.coq_top.process_response() update() update() - def show_goal(self, feedback_callback): + def show_goal(self, response): # Temporarily make the goal buffer modifiable modifiable = self.goal_buffer.options["modifiable"] self.goal_buffer.options["modifiable"] = True try: del self.goal_buffer[:] - response = self.coq_top.goals(feedback_callback) - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return False - - if isinstance(response, CT.Err): return False - if response.val.val is None: + goals = response.val + if goals is None: self.goal_buffer[0] = 'No goals.' return True - goals = response.val.val - sub_goals = goals.fg msg_format = '{0} subgoal{1}' show_hyps = True @@ -368,7 +350,7 @@ def show_info(self, message): self.info_buffer.options["modifiable"] = modifiable def clear_info(self): - self.coq_top.clear_errors() + self.coq_top.clear_messages() self.show_info(None) def convert_offset(self, range_start, offset, range_end): @@ -385,8 +367,11 @@ def reset_color(self): prev_end = None sent_start = None checked_start = None - for c in itertools.chain(self.coq_top.states): - if c.state in (CT.Command.SENT, CT.Command.ABANDONED): + commands = self.coq_top.get_commands() + for c in commands: + if c.state in (CT.Command.REVERTED, CT.Command.ABANDONED): + break + if c.state == CT.Command.SENT: if sent_start is None: # Start a sent range sent_start = prev_end @@ -395,12 +380,11 @@ def reset_color(self): sent.append(make_vim_range(sent_start, prev_end)) sent_start = None - # Count the warning and error states as checked. A subrange will - # also be marked as a warning or error, but that will override the - # checked group. - if c.state in (CT.Command.PROCESSED, - CT.Command.WARNING, - CT.Command.ERROR): + # Include all the processed commands as checked, even if they + # produced a warning or error message. A subrange will also be + # marked as a warning or error, but that will override the checked + # group. + if c.state == CT.Command.PROCESSED: if checked_start is None: # Start a checked range checked_start = prev_end @@ -416,10 +400,8 @@ def reset_color(self): # Finish a checked range checked.append(make_vim_range(checked_start, prev_end)) prev_end = None - for c in itertools.chain(self.coq_top.states, - self.coq_top.reverted_states): - if c.state in (CT.Command.WARNING, - CT.Command.ERROR): + for c in commands: + if c.msg_type != CT.Command.NONE: # Normalize the start and stop positions, if it hasn't been done yet. if c.msg_start_offset is not None and c.msg_start is None: c.msg_start = self.convert_offset(prev_end, @@ -434,7 +416,7 @@ def reset_color(self): if start == stop: start = prev_end stop = c.end - if c.state == CT.Command.WARNING: + if c.msg_type == CT.Command.WARNING: warnings.append(make_vim_range(start, stop)) else: errors.append(make_vim_range(start, stop)) @@ -458,17 +440,17 @@ def rewind_to(self, line, col): print('Please report.') return - if (self.coq_top.states and - (self.coq_top.states[-1].end[0], - self.coq_top.states[-1].end[1]) <= (line, col)): + last = self.coq_top.get_last_active_command() + if (last and (last.end[0], last.end[1]) <= (line, col)): # The caller asked to rewind to a position after what has been # processed. This quick path exits without having to search the # state list. return predicate = lambda x: (x.end[0], x.end[1]) <= (line, col) - lst = filter(predicate, self.coq_top.states) - steps = len(self.coq_top.states) - len(list(lst)) + commands = self.coq_top.get_active_commands() + lst = filter(predicate, commands) + steps = len(commands) - len(list(lst)) if steps != 0: self.coq_rewind(steps) @@ -476,7 +458,7 @@ def rewind_to(self, line, col): # Communication with Coqtop # ############################# - def send_until_fail(self): + def send_until_fail(self, send_queue): """ Tries to send every message in [send_queue] to Coq, stops at the first error. @@ -484,46 +466,22 @@ def send_until_fail(self): """ self.clear_info() - encoding = vim.eval('&fileencoding') or 'utf-8' - - while len(self.send_queue) > 0: - message_range = self.send_queue.popleft() - (eline, ecol, ebyte) = message_range['stop'] - message = self._between(message_range['start'], - (eline, ecol - 1, ebyte - 1)) - - response = self.coq_top.advance(message, - (eline, ecol, ebyte), encoding) - - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return - - if isinstance(response, CT.Ok): - optionnal_info = response.val[1] - else: - self.send_queue.clear() - if isinstance(response, CT.Err): - loc_s = response.loc_s - if loc_s is not None: - loc_e = response.loc_e - (l, c, b) = message_range['start'] - (l_start, c_start, b_start) = _pos_from_offset(c, b, - message, - loc_s) - (l_stop, c_stop, b_stop) = _pos_from_offset(c, b, - message, - loc_e) - self.error_at = ((l + l_start, c_start, b_start), - (l + l_stop, c_stop, b_stop)) - else: - print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) - break + # Start sending on a background thread + self.coq_top.send_async(send_queue) - self.reset_color() - vim.command('redraw') + # Redraw the screen when the background thread makes progress + while True: + result = self.coq_top.wait_for_result() + if result & CT.CoqTop.COMMAND_CHANGED: + self.reset_color() + vim.command('redraw') + if result & CT.CoqTop.MESSAGE_RECEIVED: + new_info = self.coq_top.get_messages() + self.show_info(new_info) + if result & CT.CoqTop.SEND_DONE: + break + self.coq_top.finish_send() self.refresh() ################# @@ -573,7 +531,11 @@ def _get_message_range(self, after): if end_pos is None: return None else: - return { 'start':after , 'stop':self._add_byte_offset(end_pos) } + end_pos = self._add_byte_offset(end_pos) + (eline, ecol, ebyte) = end_pos + message = self._between(after, + (eline, ecol - 1, ebyte - 1)) + return (message, end_pos) # A bullet is: # - One or more '-' From c79c21745574eb42a954d57a86e4c4519be8ac07 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sat, 28 Oct 2017 02:42:50 -0700 Subject: [PATCH 10/12] Show the warning highlight in the correct places in 8.7 --- autoload/coqtop.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/autoload/coqtop.py b/autoload/coqtop.py index e255440..89a1006 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -307,6 +307,10 @@ def parse_feedback(self, xml): if xml.get("object") == "state": state_id = parse_value(xml.find("state_id")) comm = self.get_command_by_state_id(state_id) + if comm is None: + # coqtop must be sending feedback for a statement before it + # sent a reply to the Add command. + comm = self.get_command_by_state_id(None) else: edit_id = parse_value(xml.find("edit_id")) comm = self.get_command_by_edit(edit_id) @@ -318,9 +322,11 @@ def parse_feedback(self, xml): level = level.get("val") if level == "error": level = Command.ERROR - else: + elif level == "warning": level = Command.WARNING - if comm: + else: + level = Command.NONE + if comm and level != Command.NONE: comm.msg_type = level # The element type is option if messageNode[1].get("val") == "some": From 01a62bf3f068db681cba109dbc777c4e4323be1e Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sat, 16 Dec 2017 13:16:18 -0800 Subject: [PATCH 11/12] Fix syncing the colors of a buffer when it is open in multiple tabs --- autoload/coquille.vim | 58 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 50 insertions(+), 8 deletions(-) diff --git a/autoload/coquille.vim b/autoload/coquille.vim index 81307ed..c2b7d8e 100644 --- a/autoload/coquille.vim +++ b/autoload/coquille.vim @@ -280,9 +280,9 @@ function! coquille#WinId2TabWin(winid, hint_tabnr, hint_winnr) endif return [l:tabnr, l:winnr] endif - let l:search_tab=1 + let l:search_tab = 1 while l:search_tab <= tabpagenr("$") - let l:search_win=1 + let l:search_win = 1 while l:search_win <= tabpagewinnr(l:search_tab, "$") if gettabwinvar(l:search_tab, l:search_win, "coquille_winid", -1) \ == a:winid @@ -422,7 +422,7 @@ endfunction " Return the window id of a window in the specified tab with the specified " filetype, with w:coquille_shared set to 1, or -1 if no such window exists function! coquille#FindSharedWin(tabnr, filetype) - let l:search_win=1 + let l:search_win = 1 let l:default_shared = !exists("g:coquille_shared") || g:coquille_shared while l:search_win <= tabpagewinnr(a:tabnr, "$") if !gettabwinvar(a:tabnr, l:search_win, "coquille_shared", @@ -472,7 +472,7 @@ function coquille#GarbageCollectSupportWin(winid) call coquille#LoadBlankBuffer(a:winid, l:tabwin[0], l:tabwin[1]) return endif - let l:search_win=1 + let l:search_win = 1 while l:search_win <= tabpagewinnr(l:tabwin[0], "$") if gettabwinvar(l:tabwin[0], l:search_win, "coquille_goal_winid", -1) \ == a:winid || @@ -683,7 +683,14 @@ endfunction let s:empty_range = [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] function! coquille#SyncWindowColors(winid, hint_tabnr, hint_winnr) + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + if l:tabwin[0] != l:cur_tab + " Only update the colors for windows in the current tab. The colors + " for windows in other tabs will be updated when their tab is entered. + return 0 + endif let l:bufnr = coquille#TabWinBufnr(l:tabwin[0], l:tabwin[1]) " Map from variable name to [group name, priority] let l:group_infos = { @@ -704,10 +711,17 @@ function! coquille#SyncWindowColors(winid, hint_tabnr, hint_winnr) endif " matchadd() only works for the current window. So switch to a:winid. if !l:switched - let l:cur_tab = tabpagenr() - let l:cur_win = winnr() let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) call coquille#WinGoToId(a:winid, l:tabwin[0], l:tabwin[1]) + let l:switched = 1 + endif + " Switching the window could have triggered the colors to get synced. + " So double check that they need to be synced. + let l:win_value = coquille#GetWinVar(a:winid, tabpagenr(), winnr(), + \ l:group, [s:empty_range, -1]) + if l:win_value[0] == l:buf_value + " It already matches; nothing to do + continue endif if l:win_value[1] != -1 call matchdelete(l:win_value[1]) @@ -724,15 +738,42 @@ function! coquille#SyncWindowColors(winid, hint_tabnr, hint_winnr) \ l:group, [l:buf_value, l:matchid]) endfor if l:switched - " Switch back to the original tab + " Switch back to the original window call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) endif + return l:switched endfunction function! coquille#SyncBufferColors(bufid) + let l:old_redraw = &lazyredraw + if !l:old_redraw + "set lazyredraw + endif + let l:need_redraw = 0 for winid in coquille#WinFindBuf(a:bufid) - call coquille#SyncWindowColors(l:winid, 0, 0) + if coquille#SyncWindowColors(l:winid, 0, 0) + let l:need_redraw = 1 + endif endfor + if !l:old_redraw + "set nolazyredraw + if l:need_redraw + "redraw + endif + endif +endfunction + +function! coquille#TabActivated() + " Colors are not synced for windows in inactive tabs, so when a tab + " becomes active, all of its colors need to be synced + let l:search_win = 1 + let l:cur_tab = tabpagenr() + let l:cur_win = 1 + while l:cur_win <= tabpagewinnr(l:cur_tab, "$") + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + call coquille#SyncWindowColors(l:cur_winid, l:cur_tab, l:cur_win) + let l:cur_win += 1 + endwhile endfunction function! coquille#WindowActivated(winid, hint_tabnr, hint_winnr) @@ -857,6 +898,7 @@ function! coquille#Register() autocmd WinEnter * call coquille#WindowActivated( \ coquille#WinGetId(tabpagenr(), winnr()), \ tabpagenr(), winnr()) + autocmd TabEnter * call coquille#TabActivated() autocmd BufWinEnter * call coquille#WindowActivated( \ coquille#WinGetId(tabpagenr(), winnr()), \ tabpagenr(), winnr()) From 727ecafe0da18018758b6873a6475f9fb695e423 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Sat, 16 Dec 2017 14:33:41 -0800 Subject: [PATCH 12/12] Scroll the goal and info buffers back to the top whenever they change --- autoload/coquille.py | 26 ++++++++++++++++++++++++++ autoload/coquille.vim | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+) diff --git a/autoload/coquille.py b/autoload/coquille.py index 6c1493e..3746831 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -49,6 +49,27 @@ def vim_repr(value): def make_vim_range(start, stop): return [[start[0] + 1, start[2] + 1], [stop[0] + 1, stop[2] + 1]] +# Return a list of all windows that are displaying the buffer, along with their +# current cursor positions. +def get_cursors_for_buffer(vim_buffer): + result = [] + for win in vim.windows: + if win.buffer is vim_buffer: + result.append((win, win.cursor)) + return result + +# Takes the list of window cursor positions from get_cursor_for_buffer. If the +# cursor position is now lower for any of the windows, they are entered to +# rescroll the window. +def fix_scroll(cursors): + refresh_now = None + for win, (row, col) in cursors: + if win.cursor[0] < row or win.cursor[1] < col: + win.vars['coquille_needs_scroll_fix'] = 1 + if win.tabpage is vim.current.tabpage: + vim.command("call coquille#FixWindowScrollTabWin(%d, %d)" % + (win.tabpage.number, win.number)) + # All the python side state associated with the vim source buffer class BufferState(object): # Dict mapping source buffer id to BufferState @@ -274,6 +295,7 @@ def show_goal(self, response): modifiable = self.goal_buffer.options["modifiable"] self.goal_buffer.options["modifiable"] = True try: + cursors = get_cursors_for_buffer(self.goal_buffer) del self.goal_buffer[:] if response is None: @@ -320,6 +342,8 @@ def show_goal(self, response): lines = map(lambda s: s.encode('utf-8'), ccl.split('\n')) self.goal_buffer.append(list(lines)) self.goal_buffer.append('') + + fix_scroll(cursors) finally: self.goal_buffer.options["modifiable"] = modifiable return True @@ -329,6 +353,7 @@ def show_info(self, message): modifiable = self.info_buffer.options["modifiable"] self.info_buffer.options["modifiable"] = True try: + cursors = get_cursors_for_buffer(self.info_buffer) del self.info_buffer[:] lst = [] if message is not None: @@ -346,6 +371,7 @@ def show_info(self, message): # extend function, and its append mostly behaves like extend. self.info_buffer[0] = lst[0] self.info_buffer.append(lst[1:]) + fix_scroll(cursors) finally: self.info_buffer.options["modifiable"] = modifiable diff --git a/autoload/coquille.vim b/autoload/coquille.vim index c2b7d8e..ea7820e 100644 --- a/autoload/coquille.vim +++ b/autoload/coquille.vim @@ -682,6 +682,36 @@ endfunction let s:empty_range = [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] +function! coquille#FixWindowScroll(winid, hint_tabnr, hint_winnr) + let l:cur_tab = tabpagenr() + let l:cur_win = winnr() + let l:tabwin = coquille#WinId2TabWin(a:winid, a:hint_tabnr, a:hint_winnr) + if l:tabwin[0] != l:cur_tab + " Only fix the scroll for windows in the current tab. The other + " windows will be fixed when their tab is entered. + return 0 + endif + + if coquille#GetWinVar(a:winid, l:tabwin[0], l:tabwin[1], + \ "coquille_needs_scroll_fix", 0) + let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) + call coquille#SetWinVar(a:winid, l:tabwin[0], l:tabwin[1], + \ "coquille_needs_scroll_fix", 0) + " When the cursor is at the last line of the buffer, then the number + " of lines in the buffer is reduced from python, vim leaves the window + " scrolled past the end. Just entering the window is enough to fix it. + call coquille#WinGoToId(a:winid, l:tabwin[0], l:tabwin[1]) + + call coquille#WinGoToId(l:cur_winid, l:cur_tab, l:cur_win) + return 1 + endif +endfunction + +function! coquille#FixWindowScrollTabWin(tabnr, winnr) + let l:winid = coquille#WinGetId(a:tabnr, a:winnr) + return coquille#FixWindowScroll(l:winid, a:tabnr, a:winnr) +endfunction + function! coquille#SyncWindowColors(winid, hint_tabnr, hint_winnr) let l:cur_tab = tabpagenr() let l:cur_win = winnr() @@ -772,8 +802,10 @@ function! coquille#TabActivated() while l:cur_win <= tabpagewinnr(l:cur_tab, "$") let l:cur_winid = coquille#WinGetId(l:cur_tab, l:cur_win) call coquille#SyncWindowColors(l:cur_winid, l:cur_tab, l:cur_win) + call coquille#FixWindowScroll(l:cur_winid, l:cur_tab, l:cur_win) let l:cur_win += 1 endwhile + endfunction function! coquille#WindowActivated(winid, hint_tabnr, hint_winnr)