aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-06-07 13:34:13 -0400
committerClément Pit-Claudel2020-06-07 13:34:13 -0400
commit761261041ee4c0f44c536d4ea18037c1ccaed2a4 (patch)
treef5a8dbc53c7d1d0f6cff86fb184039abab70ccf8 /doc/tools
parentaad87d7e7d7b68b13e33f58b8d5b5a6f824d3f38 (diff)
[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdomain.py24
1 files changed, 22 insertions, 2 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b0bbbf33b3..aec3607349 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -923,12 +923,32 @@ class CoqtopBlocksTransform(Transform):
@staticmethod
def split_lines(source):
- """Split Coq input in chunks
+ r"""Split Coq input in chunks
A chunk is a minimal sequence of consecutive lines of the input that
ends with a '.'
+
+ >>> split_lines('A.\nB.''')
+ ['A.', 'B.']
+
+ >>> split_lines('A.\n\nB.''')
+ ['A.', '\nB.']
+
+ >>> split_lines('A.\n\nB.\n''')
+ ['A.', '\nB.']
+
+ >>> split_lines("SearchPattern (_ + _ = _ + _).\n"
+ ... "SearchPattern (nat -> bool).\n"
+ ... "SearchPattern (forall l : list _, _ l l).")
+ ... # doctest: +NORMALIZE_WHITESPACE
+ ['SearchPattern (_ + _ = _ + _).',
+ 'SearchPattern (nat -> bool).',
+ 'SearchPattern (forall l : list _, _ l l).']
+
+ >>> split_lines('SearchHead le.\nSearchHead (@eq bool).')
+ ['SearchHead le.', 'SearchHead (@eq bool).']
"""
- return re.split(r"(?<=(?<!\.)\.)\s+\n", source)
+ return re.split(r"(?<=(?<!\.)\.)\n", source.strip())
@staticmethod
def parse_options(node):