Can't step through complex bullet/curly-brace
I found two issues with stepping through my proofs in coquille. First is that bullets are allowed to consist of the same bullet character repeated multiple times, so e.g. you can use the bullet --
or even ---
after bullets -
, +
, and *
. coquille stops halfway through a long bullet. Second is that the open curly brace can have a goal selector in front of it, e.g. 2: {
, and coquille just steps right past that to the next period. Either of these cases causes coquille to become out of sync with coq and valid proofs to fail.
I tried investigating and found I guess the incomplete bit of code in _find_next_chunk
, and here's an attempt at fixing it I'm trying myself. I am not sure if you are trying to avoid regexes for performance reasons or something, though, so here it is for reference. (It also seems that coquille was trying to step to the space after a bullet or curly brace rather than stopping at it; I'm not sure if this was intentional but coqide doesn't do it so I changed it to just stop at the bullet or curly brace.)
diff --git a/rplugin/python3/pycoqtop/__init__.py b/rplugin/python3/pycoqtop/__init__.py
index b37e096..b4aeb66 100644
--- a/rplugin/python3/pycoqtop/__init__.py
+++ b/rplugin/python3/pycoqtop/__init__.py
@@ -931,7 +931,7 @@ the previous dot."""
by a dot (outside of a comment, and not denoting a path).
"""
blen = len(self.buf)
- bullets = ['{', '}', '-', '+', '*']
+ bullets = ['-', '+', '*']
# We start by striping all whitespaces (including \n) from the beginning of
# the chunk.
while line < blen and self.buf[line][col:].strip() == '':
@@ -942,17 +942,34 @@ the previous dot."""
while self.buf[line][col] == ' ' or self.buf[line][col] == '\t': # FIXME: keeping the stripped line would be
col += 1 # more efficient.
-
- # Then we check if the first character of the chunk is a bullet.
+
+ # Then we check if the chunk starts with a bullet or a curly brace.
# Intially I did that only when I was sure to be in a proof (by looking in
# [encountered_dots] whether I was after a "collapsable" chunk or not), but
# 1/ that didn't play well with coq_to_cursor (as the "collapsable chunk"
# might not have been sent/detected yet).
# 2/ The bullet chars can never be used at the *beginning* of a chunk
# outside of a proof. So the check was unecessary.
+
if self.buf[line][col] in bullets:
- return (line, col + 1)
-
+ # Bullets can consist of the same bullet character repeated one or
+ # more times.
+ bullet = self.buf[line][col]
+ while self.buf[line][col] == bullet:
+ col += 1
+ return (line, col - 1)
+ elif self.buf[line][col] == '}':
+ return (line, col)
+ else:
+ # Finally we check if the chunk starts with an open curly brace.
+ # This is trickier bcause it could have a goal selector before it.
+ # FIXME: This is still not completely correct because the goal
+ # selector and brace can actually be spread out over multiple
+ # lines, but, come on.
+ open_brace_match = re.match(r'^(?:(?:\w+|\[\s*\w+\s*\])\s*:\s*)?{', self.buf[line][col:])
+ if open_brace_match:
+ return (line, col + open_brace_match.end() - 1)
+
# We might have a commentary before the bullet, we should be skiping it and
# keep on looking.
tail_len = len(self.buf[line]) - col