On Monday, March 25, 2019 at 7:18:27 AM UTC-5, john lunzer wrote:
Thank you for this. Sorry that it was kind of a let down beyond
> colorization for more languages.
>
As I said, I'm glad I did this project:
- Technically, it was a big step forward, and it turned out to be
surprisingly straightforward.
- Previously, I wondered whether it would be possible to add Leonine
coloring rules to *all* standard pygments lexers. Here's how, modulo error
handling:
def patch_lexer(self, language, lexer):
class PatchedLexer(lexer.__class__):
tokens = { << new rules >> }
return PatchedLexer()
Deriving from lexer.__class__ demonstrates *python's* power. It's a big
deal, and it probably should be part of pygments' docs.
- I understand pygments well enough, from *Leo's* point of view. It was a
big Aha that Leo's settings could completely replace pygments styles, which
don't seem all that clever to me.
- How pygments handles non-standard tokens is still a mystery to me. To be
safe, Leo catches exceptions in leo_h._get_format_from_style, something
that Jupyter's code did not do. This try/except statement is something
that bothers me, but for now it's there for safety.
- pyg_c.mainLoop fixes apparent bugs in the Jupyter code, and does so
elegantly.
In short, pygments will help some users, and was personally fulfilling. I
can't ask for more than that.
Edward
P. S. Completing this project may take a day or two more:
- At present, Leo uses the default font/color dicts in leoColorizer.py to
determine what settings should be examined. But that can't be exactly
right. Theoretically, @data extra-pygments-tokens might be needed, but I
suspect Leo won't need this any time soon.
- In any case, *all* standard pygments tokens should be present in the
default font/color dicts.
EKR
--
You received this message because you are subscribed to the Google Groups
"leo-editor" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to leo-editor+unsubscr...@googlegroups.com.
To post to this group, send email to leo-editor@googlegroups.com.
Visit this group at https://groups.google.com/group/leo-editor.
For more options, visit https://groups.google.com/d/optout.
