diff options
| author | Clément Pit-Claudel | 2020-06-07 13:34:13 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-06-07 13:34:13 -0400 |
| commit | 761261041ee4c0f44c536d4ea18037c1ccaed2a4 (patch) | |
| tree | f5a8dbc53c7d1d0f6cff86fb184039abab70ccf8 | |
| parent | aad87d7e7d7b68b13e33f58b8d5b5a6f824d3f38 (diff) | |
[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_lines
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 24 |
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): |
