aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorQuentin Carbonneaux2020-05-08 13:29:50 +0200
committerQuentin Carbonneaux2020-05-08 13:29:50 +0200
commit24497500d30a6719b2eb92c3795ab067e2cdf14f (patch)
tree814ccdf8b2c6d5877910f00484389ee90d24ed31
parent5e385d0744764cc22c66af898ed11859df0b6225 (diff)
Simplify splitting
-rw-r--r--doc/tools/coqrst/coqdomain.py20
1 files changed, 8 insertions, 12 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 253fc5283f..df11960403 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -905,17 +905,13 @@ class CoqtopBlocksTransform(Transform):
return isinstance(node, nodes.Element) and 'coqtop_options' in node
@staticmethod
- def split_sentences(node):
- """Split Coq sentences in source. Could be improved."""
- lines = map(lambda s: s.rstrip(), node.rawsource.splitlines())
- out = [""]
- for l in lines:
- out[-1] = out[-1] + l + "\n"
- if l.endswith("."):
- out.append("")
- if out[-1] == "":
- out.pop()
- return out
+ def split_lines(source):
+ """Split Coq input in chunks
+
+ A chunk is a minimal sequence of consecutive lines of the input that
+ ends with a '.'
+ """
+ return re.split(r"(?<=(?<!\.)\.)\s+\n", source)
@staticmethod
def parse_options(node):
@@ -994,7 +990,7 @@ class CoqtopBlocksTransform(Transform):
repl.sendone('Unset Coqtop Exit On Error.')
if options['warn']:
repl.sendone('Set Warnings "default".')
- for sentence in self.split_sentences(node):
+ for sentence in self.split_lines(node.rawsource):
pairs.append((sentence, repl.sendone(sentence)))
if options['abort']:
repl.sendone('Abort All.')