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 8d35600..89a1006 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -1,17 +1,30 @@ +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 +import threading from collections import deque, namedtuple +# Define unicode in python 3 +if isinstance(__builtins__, dict): + unicode = __builtins__.get('unicode', str) +else: + unicode = getattr(__builtins__, 'unicode', str) + Ok = namedtuple('Ok', ['val', 'msg']) -Err = namedtuple('Err', ['err']) +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']) @@ -29,8 +42,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 ' @@ -48,6 +62,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': @@ -86,7 +102,20 @@ 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') + 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(msg, revert_state, int(loc_s), int(loc_e)) + else: + return Err(msg, revert_state, None, None) def build(tag, val=None, children=()): attribs = {'val': val} if val is not None else {} @@ -104,7 +133,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 @@ -112,6 +141,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): @@ -135,141 +166,465 @@ 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) def escape(cmd): - return cmd.replace(" ", ' ') \ + escaped = cmd.replace(" ", ' ') \ .replace("'", '\'') \ .replace("(", '(') \ .replace(")", ')') + if isinstance(escaped, str): + return escaped + else: + return escaped.encode('ascii', 'xmlcharrefreplace') -def get_answer(): - fd = coqtop.stdout.fileno() - data = '' - while True: - try: - data += os.read(fd, 0x4000) +class Command(object): + # Values for self.state + # ---------------------- + # Command was sent to coqtop through an Add call, and coq acknowledged the + # Add. + SENT = 0 + # 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 = 1 + # coqtop sent an error level message for the command through a feedback + # statement. + ERROR = 2 + + 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, 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 + 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 + # 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): + # bit fields for self.result + COMMAND_CHANGED = 1 + MESSAGE_RECEIVED = 2 + SEND_DONE = 4 + + 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.messages = [] + + self.lock = threading.Lock() + self.result = 0 + self.has_result = threading.Condition(self.lock) + self.send_thread = None + + 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 + 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 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_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) + 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 + elif level == "warning": + level = Command.WARNING + 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": + 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.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]) + 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[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. + 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): + assert xml.tag == 'message' + level = xml.find('message_level') + if level is not None: + level = level.get('val') + 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.msg_type = Command.WARNING + self.messages.append(parse_value(xml[2])) + + def process_response(self): + fd = self.coqtop.stdout.fileno() + data = u'' + while True: 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': + data += os.read(fd, 0x4000).decode("utf-8") + try: + elt = ET.fromstring('' + escape(data) + '') + 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: - messageNode = messageNode + "\n\n" + parse_value(c[2]) - else: - messageNode = parse_value(c[2]) - if shouldWait: + 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: + # 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, feedback_callback=None): + xml = encode_call(name, arg) + msg = ET.tostring(xml, 'utf-8') + 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: + with self.lock: + if os.name == 'nt': + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , stderr = subprocess.STDOUT + ) else: - vp = parse_response(valueNode) - if messageNode is not None: - if isinstance(vp, Ok): - return Ok(vp.val, messageNode) - return vp - except ET.ParseError: - continue - except OSError: - # coqtop died - return None + self.coqtop = subprocess.Popen( + options + list(args) + , stdin = subprocess.PIPE + , stdout = subprocess.PIPE + , preexec_fn = ignore_sigint + ) -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 + r = self.call('Init', Option(None)) + 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 -def advance(cmd, encoding = 'utf-8'): - global state_id - r = call('Add', ((cmd, -1), (cur_state(), True)), encoding) - if r is None: - return r - if isinstance(r, Err): + def launch_coq(self, *args): + return self.restart_coq(*args) + + def cur_state(self): + self.check_state_indexes() + return self.states[self.reverted_index - 1].state_id + + # 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_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))) + 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 + + def rewind(self, step = 1, keep_states = False): + 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 - 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): + 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.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 67e54f3..3746831 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -1,567 +1,722 @@ +from __future__ import print_function +from __future__ import unicode_literals +from __future__ import division + import vim 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 - -info_msg = None - -################### -# synchronization # -################### - -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 _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() - -##################### -# exported commands # -##################### - -def kill_coqtop(): - CT.kill_coqtop() - _reset() - -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(steps=1): - clear_info() - - global encountered_dots, info_msg - - if steps < 1 or encountered_dots == []: - return +vimbufsync.check_version([0,1,0], who="coquille") + +# Define unicode in python 3 +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')") + +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, byte) tuples into 1-based lists in the form +# [line, byte] +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 + 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 + 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 - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + ################### + # synchronization # + ################### - response = CT.rewind(steps) + def sync(self): + curr_sync = vimbufsync.sync(self.source_buffer) + if not self.saved_sync or curr_sync.buf() != self.saved_sync.buf(): + if self.coq_top.get_active_command_count() > 1: + self._reset() + else: + (line, col) = self.saved_sync.pos() + # vim indexes from lines 1, coquille from 0 + self.rewind_to(line - 1, col - 1) + self.saved_sync = curr_sync + + def _reset(self): + self.coq_top.kill_coqtop() + self.saved_sync = None + self.reset_color() + + ##################### + # exported commands # + ##################### + + def kill_coqtop(self): + if self is None: + return + self._reset() - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return + def goto_last_sent_dot(self): + 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) - if isinstance(response, CT.Ok): - encountered_dots = encountered_dots[:len(encountered_dots) - steps] - else: - info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response + def coq_rewind(self, steps=1): + self.clear_info() - refresh() + # Do not allow the root state to be rewound + if steps < 1 or self.coq_top.get_active_command_count() < 2: + 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'): - goto_last_sent_dot() + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return -def coq_to_cursor(): - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + response = self.coq_top.rewind(steps) - sync() + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - (cline, ccol) = vim.current.window.cursor - (line, col) = encountered_dots[-1] if encountered_dots else (0,0) + self.refresh() - 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 + # 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() - send_until_fail() + 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 -def coq_next(): - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + self.sync() - sync() + (cline, ccol) = vim.current.window.cursor + cline -= 1 + last = self.coq_top.get_last_active_command() + last_sent = ((0,0,0) if not last else last.end) + (line, col, byte) = last_sent - (line, col) = encountered_dots[-1] if encountered_dots else (0,0) - message_range = _get_message_range((line, col)) + 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, ccol + 1) + else: + send_queue = deque([]) + while True: + r = self._get_message_range(last_sent) + if (r is not None + and (r[1][0], r[1][1]) <= (cline, ccol + 1)): + last_sent = r[1] + send_queue.append(r) + else: + break + + self.send_until_fail(send_queue) + + def coq_next(self): + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - if message_range is None: return + self.sync() - send_queue.append(message_range) + 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) - send_until_fail() + if message_range is None: return - if (vim.eval('g:coquille_auto_move') == 'true'): - goto_last_sent_dot() + send_queue = deque([]) + send_queue.append(message_range) -def coq_raw_query(*args): - clear_info() + self.send_until_fail(send_queue) - global info_msg - if CT.coqtop is None: - print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") - return + if (vim.eval('g:coquille_auto_move') == 'true'): + self.goto_last_sent_dot() - raw_query = ' '.join(args) + def coq_raw_query(self, *args): + self.clear_info() - encoding = vim.eval("&encoding") or 'utf-8' + if self.coq_top.coqtop is None: + print("Error: Coqtop isn't running. Are you sure you called :CoqLaunch?") + return - response = CT.query(raw_query, encoding) + raw_query = ' '.join(args) - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') - return + response = self.coq_top.query(raw_query) - if isinstance(response, CT.Ok): - if response.msg is not None: - info_msg = response.msg - elif isinstance(response, CT.Err): - info_msg = response.err.text - print("FAIL") - else: - print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) # ugly + if response is None: + vim.command("call coquille#KillSession()") + print('ERROR: the Coq process died') + return - show_info() + info_msg = self.coq_top.get_messages() + self.show_info(info_msg) -def launch_coq(*args): - CT.restart_coq(*args) + 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(): - if encountered_dots: + def debug(self): + commands = self.coq_top.get_active_commands() print("encountered dots = [") - for (line, col) in encountered_dots: + for (line, col) in commands: 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 response.msg is not None: - info_msg = response.msg - - 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) + ##################################### + # IDE tools: Goal, Infos and colors # + ##################################### + + def refresh(self): + last_info = [None] + def update(): + self.reset_color() + vim.command('redraw') + new_info = self.coq_top.get_messages() + if last_info[0] != new_info: + self.show_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 + # commands finished. + 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, response): + # Temporarily make the goal buffer modifiable + 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: + return False + + goals = response.val + if goals is None: + self.goal_buffer[0] = 'No goals.' + return True + + 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) + 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 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')) + self.goal_buffer.append(list(lines)) + self.goal_buffer.append('') + + fix_scroll(cursors) + finally: + self.goal_buffer.options["modifiable"] = modifiable + return True - if response is None: - vim.command("call coquille#KillSession()") - print('ERROR: the Coq process died') + def show_info(self, message): + # Temporarily make the info buffer modifiable + 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: + 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:]) + fix_scroll(cursors) + finally: + self.info_buffer.options["modifiable"] = modifiable + + def clear_info(self): + self.coq_top.clear_messages() + self.show_info(None) + + def convert_offset(self, range_start, offset, range_end): + message = self._between(range_start, range_end) + (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 = [] + checked = [] + warnings = [] + errors = [] + prev_end = None + sent_start = None + checked_start = None + 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 + elif sent_start is not None: + # Finish a sent range + sent.append(make_vim_range(sent_start, prev_end)) + sent_start = None + + # 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 + 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 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, + 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.msg_type == 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): + """ 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 isinstance(response, CT.Ok): - (eline, ecol) = message_range['stop'] - encountered_dots.append((eline, ecol + 1)) - - optionnal_info = response.val[1] - if len(response.val) > 1 and isinstance(response.val[1], tuple): - info_msg = response.val[1][1] - else: - send_queue.clear() - if isinstance(response, CT.Err): - response = response.err - info_msg = response.text - loc_s = response.get('loc_s') - if loc_s is not None: - loc_s = int(loc_s) - loc_e = int(response.get('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)) - else: - print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) - break + 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 - refresh() + predicate = lambda x: (x.end[0], x.end[1]) <= (line, col) + commands = self.coq_top.get_active_commands() + lst = filter(predicate, commands) + steps = len(commands) - len(list(lst)) + if steps != 0: + self.coq_rewind(steps) + + ############################# + # Communication with Coqtop # + ############################# + + def send_until_fail(self, send_queue): + """ + 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() + + # Start sending on a background thread + self.coq_top.send_async(send_queue) + + # 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 -def _pos_from_offset(col, msg, offset): - str = msg[:offset] - lst = str.split('\n') - 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) + self.coq_top.finish_send() + self.refresh() + + ################# + # 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, 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, byte) = after + end_pos = self._find_next_chunk(line, col) + if end_pos is None: + return None + else: + 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 '-' + # - 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. + 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) + # We start by striping all whitespaces (including \n) from the beginning of + # the chunk. + 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 + + # 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. + 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(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 - return _find_dot_after(line, col) + return self._find_next_chunk(line, col) + + + # If the chunk doesn't start with a bullet, we look for a dot. + dot = self._find_dot_after(line, col) + if dot: + # Return the position one after the dot + return (dot[0], dot[1] + 1) 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) + return None + + 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._get_remaining_line(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._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._get_remaining_line(line, col + dot_pos - 2)[0] == '.': + # But we want to capture "..." + return (line, dot_pos + col) + else: + return self._find_dot_after(line, col + dot_pos + 1) 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, 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._get_remaining_line(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._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): + col += com_end + 2 + nb_left -= 1 + elif com_start > -1: + col += com_start + 2 + nb_left += 1 + else: + line += 1 + col = 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) +def _empty_range(): + return [ { 'line': 0, 'col': 0}, { 'line': 0, 'col': 0} ] + +# 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) + byte = len(lst[-1].encode("utf-8")) + (byte if line == 0 else 0) + return (line, col, byte) diff --git a/autoload/coquille.vim b/autoload/coquille.vim index 0e5045f..ea7820e 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,45 +115,824 @@ 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 +" 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 + +function! coquille#KillSession() + let l:winid = coquille#WinGetId(tabpagenr(), winnr()) + let l:bufid = coquille#TabWinBufnr(tabpagenr(), winnr()) + + call coquille#DetachSupportingBuffers(l:bufid) + + " 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 the cursor moves while in insert + " mode. Typically this happens when the buffer is modified. Syncing + " the buffer is useful 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 CursorMovedI call coquille#Python('" + \ "coquille.BufferState.lookup_bufid(". + \ a:bufid . ").sync()')" " initialize the plugin (launch coqtop) - py coquille.launch_coq(*vim.eval("map(copy(a:000),'expand(v:val)')")) + 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 - " 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#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 - command! -buffer -nargs=* Coq call coquille#RawQuery() +" 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 - call coquille#ShowPanels() +" 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 - " 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') - au InsertEnter py coquille.sync() +" 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 -function! coquille#Register() - hi default CheckedByCoq ctermbg=17 guibg=LightGreen - hi default SentToCoq ctermbg=60 guibg=LimeGreen +" 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#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() + 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 = { + \ "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_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]) + 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 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) + 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) + 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) + " 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 TabEnter * call coquille#TabActivated() + 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")