diff options
| author | Quentin Carbonneaux | 2020-05-08 13:29:50 +0200 |
|---|---|---|
| committer | Quentin Carbonneaux | 2020-05-08 13:29:50 +0200 |
| commit | 24497500d30a6719b2eb92c3795ab067e2cdf14f (patch) | |
| tree | 814ccdf8b2c6d5877910f00484389ee90d24ed31 | |
| parent | 5e385d0744764cc22c66af898ed11859df0b6225 (diff) | |
Simplify splitting
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 20 |
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.') |
