transforms: Enhance the marker DSL to allow setting properties

This allows `.path[key]=val` annotations.  For now Alectryon only supports one
property, `[lang]`, which specifies which lexer to use to highlight a particular
fragment of code (though technically, since +- polarities get translated into
the "enabled" property, specifying `[enabled]=…` would also work to enable the
display of a particular piece of code).

Author: cpitclaudel

alectryon/core.py

@@ -21,6 +21,7 @@
 from typing import Any, Iterator, List, Tuple, Union, NamedTuple
 
 from collections import namedtuple, defaultdict
+from contextlib import contextmanager
 from shlex import quote
 from shutil import which
 from subprocess import Popen, PIPE, check_output
@@ -62,14 +63,14 @@ class Enriched():
     def __new__(cls, *args, **kwargs):
         if len(args) < len(getattr(super(), "_fields", ())):
             # Don't repeat fields given by position (it breaks pickle & deepcopy)
-            kwargs = {"ids": [], "markers": [], "flags": {}, **kwargs}
+            kwargs = {"ids": [], "markers": [], "props": {}, **kwargs}
         return super().__new__(cls, *args, **kwargs)
 
 def _enrich(nt):
     # LATER: Use dataclass + multiple inheritance; change `ids` and `markers` to
     # mutable `id` and `marker` fields.
     name = "Rich" + nt.__name__
-    fields = nt._fields + ("ids", "markers", "flags")
+    fields = nt._fields + ("ids", "markers", "props")
     # Using ``type`` this way ensures compatibility with pickling
     return type(name, (Enriched, namedtuple(name, fields)),
                 {"__slots__": ()})
@@ -96,15 +97,28 @@ def __call__(self, prefix):
         self.counters[prefix] += 1
         return self.stem + prefix + b16(self.counters[prefix])
 
-class Backend: # pylint: disable=no-member
+@contextmanager
+def nullctx():
+    yield
+
+class Backend:
+    def __init__(self, highlighter):
+        self.highlighter = highlighter
+
     def gen_sentence(self, s): raise NotImplementedError()
     def gen_hyp(self, hyp): raise NotImplementedError()
     def gen_goal(self, goal): raise NotImplementedError()
     def gen_message(self, message): raise NotImplementedError()
     def highlight(self, s): raise NotImplementedError()
     def gen_names(self, names): raise NotImplementedError()
+    def gen_code(self, code): raise NotImplementedError()
     def gen_txt(self, s): raise NotImplementedError()
 
+    def highlight_enriched(self, obj):
+        lang = obj.props.get("lang")
+        with self.highlighter.override(lang=lang) if lang else nullctx():
+            return self.highlight(obj.contents)
+
     def _gen_any(self, obj):
         if isinstance(obj, (Text, RichSentence)):
             self.gen_sentence(obj)
@@ -115,7 +129,7 @@ def _gen_any(self, obj):
         elif isinstance(obj, RichMessage):
             self.gen_message(obj)
         elif isinstance(obj, RichCode):
-            self.highlight(obj.contents)
+            self.gen_code(obj)
         elif isinstance(obj, Names):
             self.gen_names(obj)
         elif isinstance(obj, str):

alectryon/docutils.py

@@ -485,7 +485,7 @@ def _find_mref_target(cls, path, ios, last_io):
                 # Unfold to ensure visibility (but only if search succeeded)
                 if sentence.annots.unfold is None:
                     sentence.annots.unfold = True
-                goal.flags.setdefault("unfold", True)
+                goal.props.setdefault("unfold", True)
                 if "type" in path:
                     return hyp.type
                 if "body" in path:
@@ -581,7 +581,7 @@ def replace_one_io(cls, node, fmt, generator):
 
     @classmethod
     def replace_one_quote(cls, node, fmt, generator):
-        target = transforms.strip_ids_and_flags(deepcopy(node.details["target"]))
+        target = transforms.strip_ids_and_props(deepcopy(node.details["target"]), {"enabled"})
         cls.replace_one(node, fmt, node.details["path"], generator.gen_part,
                         target, inline=node.details["inline"])
 

alectryon/html.py

@@ -18,7 +18,6 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from contextlib import contextmanager
 from functools import wraps
 from os import path
 import pickle
@@ -27,7 +26,7 @@
 from dominate.util import text as txt
 
 from . import transforms, GENERATOR
-from .core import b16, Gensym, Backend, Text, RichSentence, Goals, Messages, Asset
+from .core import b16, nullctx, Gensym, Backend, Text, RichSentence, Goals, Messages, Asset
 
 _SELF_PATH = path.dirname(path.realpath(__file__))
 
@@ -90,13 +89,9 @@ def _fn(self, *args, **kwargs):
         return _fn
     return _deduplicate
 
-@contextmanager
-def nullctx():
-    yield
-
 class HtmlGenerator(Backend):
     def __init__(self, highlighter, gensym_stem="", minify=False):
-        self.highlighter = highlighter
+        super().__init__(highlighter)
         self.gensym = None if minify else Gensym(gensym_stem + "-" if gensym_stem else "")
         self.minify, self.backrefs = minify, ({} if minify else None)
 
@@ -110,9 +105,9 @@ def gen_clickable(toggle, cls, *contents):
     def highlight(self, s):
         return self.highlighter(s)
 
-    def gen_code(self, dom, code, **kwargs):
-        with dom(self.highlight(code.contents), **kwargs):
-            self.gen_mrefs(code)
+    def gen_code(self, code):
+        self.highlight_enriched(code)
+        self.gen_mrefs(code)
 
     @staticmethod
     def gen_names(names):
@@ -126,10 +121,12 @@ def gen_hyp(self, hyp):
                 if hyp.body:
                     with tags.span(cls="hyp-body"):
                         tags.b(":= ")
-                        self.gen_code(tags.span, hyp.body)
+                        with tags.span():
+                            self.gen_code(hyp.body)
                 with tags.span(cls="hyp-type"):
                     tags.b(": ")
-                    self.gen_code(tags.span, hyp.type)
+                    with tags.span():
+                        self.gen_code(hyp.type)
             self.gen_mrefs(hyp)
 
     @deduplicate(".goal-hyps")
@@ -141,7 +138,8 @@ def gen_hyps(self, hyps):
 
     @deduplicate(".goal-conclusion")
     def gen_ccl(self, conclusion):
-        self.gen_code(tags.div, conclusion, cls="goal-conclusion")
+        with tags.div(cls="goal-conclusion"):
+            self.gen_code(conclusion)
 
     @deduplicate(".alectryon-goal")
     def gen_goal(self, goal, toggle=None): # pylint: disable=arguments-differ
@@ -176,7 +174,7 @@ def gen_extra_goals(self, goals):
         with tags.div(cls='alectryon-extra-goals'):
             for goal in goals:
                 toggle = goal.hypotheses and \
-                    self.gen_checkbox(goal.flags.get("unfold"),
+                    self.gen_checkbox(goal.props.get("unfold"),
                                       "alectryon-extra-goal-toggle")
                 self.gen_goal(goal, toggle=toggle)
 
@@ -190,13 +188,12 @@ def gen_goals(self, goals):
 
     def gen_input(self, fr, toggle):
         cls = "alectryon-input" + (" alectryon-failed" if fr.annots.fails else "")
-        with self.gen_clickable(toggle, cls, self.highlight(fr.input.contents)):
+        with self.gen_clickable(toggle, cls, self.highlight_enriched(fr.input)):
             self.gen_mrefs(fr)
             self.gen_mrefs(fr.input)
 
     def gen_message(self, message):
-        self.highlight(message.contents)
-        self.gen_mrefs(message)
+        self.gen_code(message)
 
     @deduplicate(".alectryon-output")
     def gen_output(self, fr):

alectryon/latex.py

@@ -182,14 +182,11 @@ def __getattribute__(self, macro_name):
 macros = Macros()
 
 class LatexGenerator(Backend):
-    def __init__(self, highlighter):
-        self.highlighter = highlighter
-
     def highlight(self, s):
         return [Raw(self.highlighter(s, prefix="", suffix=""), verbatim=True)]
 
     def gen_code(self, code):
-        with Concat(*self.highlight(code.contents)) as block:
+        with Concat(*self.highlight_enriched(code)) as block:
             self.gen_mrefs(code)
             return block
 

alectryon/pygments.py

@@ -193,11 +193,6 @@ def highlight_latex(code, lang,
 
 HIGHLIGHTERS = {"html": highlight_html, "latex": highlight_latex}
 
-def make_highlighter(fmt, lang, style=None):
-    highlighter = HIGHLIGHTERS[fmt]
-    return lambda s, *args, **kwargs: \
-        highlighter(s, *args, **{"style": style, "lang": lang, **kwargs}) # type: ignore
-
 @contextmanager
 def munged_dict(d, updates):
     saved = d.copy()
@@ -207,6 +202,23 @@ def munged_dict(d, updates):
     finally:
         d.update(saved)
 
+class Highlighter: # LATER: dataclass
+    def __init__(self, fmt, lang, style=None):
+        self.kwargs = {"lang": lang, "style": style}
+        self.highlighter = HIGHLIGHTERS[fmt]
+
+    def __call__(self, code, **kwargs):
+        return self.highlighter(code, **{**self.kwargs, **kwargs})
+
+    @contextmanager
+    def override(self, **kwargs):
+        assert set(kwargs.keys()) <= {"lang", "style"}
+        with munged_dict(self.kwargs, kwargs):
+            yield
+
+def make_highlighter(fmt, lang, style=None):
+    return Highlighter(fmt, lang, style)
+
 class WarnOnErrorTokenFilter(Filter):
     """Print a warning when the lexer generates an error token."""
 

alectryon/transforms.py

@@ -32,14 +32,14 @@
     RichHypothesis, RichGoal, RichMessage, RichCode, \
     Goals, Messages, RichSentence
 
-PathAnnot = namedtuple("PathAnnot", "enabled path")
+PathAnnot = namedtuple("PathAnnot", "path key val")
 
 class IOAnnots:
     def __init__(self):
         self.filters = None
         self.unfold = None
         self.fails = None
-        self.paths = []
+        self.props = []
 
     NO = re.compile("no-")
     RE = re.compile("(?P<io>[-a-z]+)")
@@ -77,8 +77,8 @@ def update(self, annot):
                     raise ValueError("Unknown flag `{}`.".format(flag))
                 self.filters[flag] = not negated
 
-    def update_paths(self, polarity, path):
-        self.paths.append(PathAnnot(polarity != "-", path))
+    def update_props(self, path, key, val):
+        self.props.append(PathAnnot(path, key, val))
 
     @property
     def hidden(self):
@@ -93,8 +93,8 @@ def __getitem__(self, key):
         return self.filters[key] if self.filters else True
 
     def __repr__(self):
-        return "IOAnnots(unfold={}, fails={}, filters={}, paths={})".format(
-            self.unfold, self.fails, self.filters, self.paths)
+        return "IOAnnots(unfold={}, fails={}, filters={}, props={})".format(
+            self.unfold, self.fails, self.filters, self.props)
 
 def _enrich_goal(g):
     return RichGoal(g.name,
@@ -115,7 +115,11 @@ def enrich_sentences(fragments):
             yield fr
 
 ISOLATED = r"(?:\s|\A){}(?=\s|\Z)"
-POLARIZED_PATH_SEGMENT = r"(?P<polarity>[-+]?)(?P<path>(?:{})+)".format(
+POLARIZED_PATH_SEGMENT = r"""
+  (?P<polarity>[-+]?)
+  (?P<path>(?:{})+)
+  (?:\[(?P<key>[a-z]+)\]=(?P<value>[A-Za-z0-9_]+))?
+""".format(
     markers.MARKER_PATH_SEGMENT.pattern)
 
 ONE_IO_FLAG = r"(?:{}|{})".format(
@@ -151,11 +155,13 @@ def _parse_path(path):
 
 def _update_io_flags(annots, flags_str, regex):
     for mannot in regex.finditer(flags_str):
-        io, path, polarity = mannot.group("io", "path", "polarity")
+        io, path, polarity, key, val = mannot.group("io", "path", "polarity", "key", "value")
         if io:
             annots.update(io)
         else:
-            annots.update_paths(polarity, _parse_path(path))
+            if not key:
+                key, val = "enabled", polarity != "-"
+            annots.update_props(_parse_path(path), key, val)
 
 def read_io_flags(annots, flags_str):
     _update_io_flags(annots, flags_str, ONE_IO_FLAG_RE)
@@ -218,7 +224,7 @@ def _find_marked(sentence, path):
     else:
         yield sentence
 
-def _find_flagged(sentence):
+def _find_hidden_by_annots(sentence):
     annots = sentence.annots
     if not annots["in"]:
         yield sentence.input
@@ -233,31 +239,32 @@ def _find_flagged(sentence):
             yield m
 
 def process_io_annots(fragments):
-    """Convert IO annotations to "enabled" flags."""
+    """Convert IO annotations to pre-object properties."""
     for fr in fragments:
         if isinstance(fr, RichSentence):
-            for (enabled, path) in fr.annots.paths:
+            for (path, key, val) in fr.annots.props:
                 for obj in _find_marked(fr, path):
-                    obj.flags["enabled"] = enabled
-            for obj in _find_flagged(fr):
-                obj.flags["enabled"] = False
+                    obj.props[key] = val
+
+            for obj in _find_hidden_by_annots(fr):
+                obj.props["enabled"] = False
 
             for g in fragment_goals(fr):
                 if not any(_enabled(h) for h in g.hypotheses) and not _enabled(g.conclusion):
-                    g.flags["enabled"] = False
+                    g.props["enabled"] = False
 
             any_output = any(_enabled(o) for os in fr.outputs for o in _output_objects(os))
 
             if not _enabled(fr.input) and not any_output:
-                fr.flags["enabled"] = False
+                fr.props["enabled"] = False
 
             if not fr.annots.unfold and not _enabled(fr.input) and any_output:
                 MSG = "Cannot show output of {!r} without .in or .unfold."
                 yield ValueError(MSG.format(fr.input.contents))
         yield fr
 
 def _enabled(o):
-    return o.flags.get("enabled", True)
+    return o.props.get("enabled", True)
 
 def _commit_enabled(objs):
     objs[:] = [o for o in objs if _enabled(o)]
@@ -322,12 +329,13 @@ def _sub_objects(obj):
         return ()
     assert False
 
-def strip_ids_and_flags(obj):
+def strip_ids_and_props(obj, props):
     if isinstance(obj, Enriched):
         obj.ids.clear() # type: ignore
-        obj.flags.clear() # type: ignore
+        for p in props:
+            obj.props.pop(p, None) # type: ignore
         for obj_ in _sub_objects(obj):
-            strip_ids_and_flags(obj_)
+            strip_ids_and_props(obj_, props)
     return obj
 
 LEADING_BLANKS_RE = re.compile(r'\A([ \t]*(?:\n|\Z))?(.*?)([ \t]*)\Z',