diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /doc/tools/coqrst/coqdoc/main.py | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'doc/tools/coqrst/coqdoc/main.py')
-rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py new file mode 100644 index 00000000..57adcb28 --- /dev/null +++ b/doc/tools/coqrst/coqdoc/main.py @@ -0,0 +1,91 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## +""" +Use CoqDoc to highlight Coq snippets +==================================== + +Pygment's Coq parser isn't the best; instead, use coqdoc to highlight snippets. +Only works for full, syntactically valid sentences; on shorter snippets, coqdoc +swallows parts of the input. + +Works by reparsing coqdoc's output into the output that Sphinx expects from a +lexer. +""" + +import os +import platform +from tempfile import mkstemp +from subprocess import check_output + +from bs4 import BeautifulSoup +from bs4.element import NavigableString + +COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', + '-s', '--html', '--stdout', '--utf8'] + +COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] +COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) + +def coqdoc(coq_code, coqdoc_bin=None): + """Get the output of coqdoc on coq_code.""" + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") + fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") + if platform.system().startswith("CYGWIN"): + # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." + filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip() + try: + os.write(fd, COQDOC_HEADER.encode("utf-8")) + os.write(fd, coq_code.encode("utf-8")) + os.close(fd) + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8") + finally: + os.remove(filename) + +def is_whitespace_string(elem): + return isinstance(elem, NavigableString) and elem.strip() == "" + +def strip_soup(soup, pred): + """Strip elements maching pred from front and tail of soup.""" + while soup.contents and pred(soup.contents[-1]): + soup.contents.pop() + + skip = 0 + for elem in soup.contents: + if not pred(elem): + break + skip += 1 + + soup.contents[:] = soup.contents[skip:] + +def lex(source): + """Convert source into a stream of (css_classes, token_string).""" + coqdoc_output = coqdoc(source) + soup = BeautifulSoup(coqdoc_output, "html.parser") + root = soup.find(class_='code') + strip_soup(root, is_whitespace_string) + for elem in root.children: + if isinstance(elem, NavigableString): + yield [], elem + elif elem.name == "span": + cls = "coqdoc-{}".format(elem['title']) + yield [cls], elem.string + elif elem.name == 'br': + pass + else: + raise ValueError(elem) + +def main(): + """Lex stdin (for testing purposes)""" + import sys + for classes, text in lex(sys.stdin.read()): + print(repr(text) + "\t" ' '.join(classes)) + +if __name__ == '__main__': + main() |