1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
"""Generates pygments style sheet from jupyterlab-pygments.
Source: https://github.com/jupyterlab/jupyterlab_pygments
"""
from pathlib import Path
from jupyterlab_pygments import JupyterStyle
from pygments.formatters import HtmlFormatter
prefix = """
/*-----------------------------------------------------------------------------
| Copyright (c) Jupyter Development Team.
| Distributed under the terms of the Modified BSD License.
|----------------------------------------------------------------------------*/
/* This file was auto-generated by generate_css.py in jupyterlab_pygments */
"""
def main():
formatter = HtmlFormatter(style=JupyterStyle)
css = formatter.get_style_defs('.highlight')
highlight_css = '\n'.join(filter(
lambda line: line.startswith('.highlight'), css.splitlines()
))
here = Path(__file__).parent
style_file = here / "style" / "base.css"
style_file.write_text("\n".join((prefix, highlight_css)))
if __name__ == "__main__":
main()
|
