style: pep8 style for python files

licenses: convert license tags to SPDX

misc/pysymbols: Move IsaSymbolsException to a separate file.

misc/pysymbols: Support for sub/superscripts in code blocks.

Inline code from a Markdown source (`like this`) is typically translated
without the assistance of Pygments. As a result we don't get automatic
subscript and superscript support, and need to roll our own. This translation
is pretty blunt and fragile. Expect it to fall over in a TeX error if you pass,
e.g., a "\<^bsub>" without a closing "\<^esub>".

misc/pysymbols: Add support for encoding to TeX.

You probably do *not* want to use this functionality to go straight from THY
files to TeX. The motivation for this is translating inline code in Markdown
(`like this`) into something TeX-able. In particular, we assume all relevant
Isabelle styles and preamble are already in scope.

misc/pysymbols: Don't translate entities like "\<^bsub>" into unicode.

The code points of the xsymbols whose ASCII text begins with "\<^" appear to be
a ruse. Their unicode characters do not correspond to their intent because
they are actually format markers. For example, "\<^bsub>" maps to something
described as "south east double arrow," but is intended to mean "start
subscript."

It turns out we do not need to encode these at all because a sufficiently
clever Pygments can interpret their ASCII representations. One such clever
instance is [0]. This commit removes encoding of all symbols whose ASCII
representation begins with "\<^" under the assumption they will be handled by a
later tool in your pipeline.

[0]: https://bitbucket.org/lsf37/pygments-main/branch/sub-super

misc/pysymbols: Optimise unicode to ASCII translation.

With larger THY snippets, this translation can become a noticeable bottleneck.

misc: Support for space translation in etc/symbols decoding.

See 74eddfef841e of Isabelle itself for the changeset that implements it.

misc: Add a Python module for dealing with Isabelle symbols.