docutils, html, latex: Rename href role to mref (m[arker] ref[erence])

alectryon/assets/alectryon.css

@@ -58,7 +58,7 @@ SOFTWARE.
 .alectryon-coqdoc .doc .code,
 .alectryon-coqdoc .doc .comment,
 .alectryon-coqdoc .doc .inlinecode,
-.alectryon-href,
+.alectryon-mref,
 pre.alectryon-io, .alectryon-toggle-label, .alectryon-banner {
     font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace;
     font-feature-settings: "XV00" 1; /* Use Coq ligatures when Iosevka is available */
@@ -90,8 +90,8 @@ In any case, make an exception for comments:
 }
 */
 
-.alectryon-href,
-.alectryon-href-marker {
+.alectryon-mref,
+.alectryon-mref-marker {
     align-self: center;
     box-sizing: border-box;
     display: inline-block;
@@ -103,18 +103,18 @@ In any case, make an exception for comments:
     text-decoration: none;
 }
 
-.alectryon-io .alectryon-href-marker {
+.alectryon-io .alectryon-mref-marker {
     user-select: none;
     margin: -0.25em 0 -0.25em 0.5em;
 }
 
-.alectryon-href {
+.alectryon-mref {
     color: inherit;
     margin: -0.5em 0.25em;
 }
 
-.alectryon-goal:target .goal-separator .alectryon-href-marker,
-:target > .alectryon-href-marker {
+.alectryon-goal:target .goal-separator .alectryon-mref-marker,
+:target > .alectryon-mref-marker {
     animation: blink 0.2s step-start 0s 3 normal none;
     background-color: #fcaf3e;
     position: relative;

alectryon/assets/alectryon.sty

@@ -125,7 +125,7 @@
 % improve the spacing we give it 0 depth.
 \newcommand{\alectryon@strut}{\rule[0pt]{0pt}{\ht\strutbox}}
 % \alectryon@label inserts a label and a phantomsection
-\newcommand{\alectryon@hreflabel}[1]{\phantomsection\label{#1}}
+\newcommand{\alectryon@anchor}[1]{\phantomsection\label{#1}}
 % alectryon@outer wraps collections of goals and messages
 \newenvironment{alectryon@outer}
   {\begin{tcolorbox}[colframe=alectryon@tango@medium@gray, colback=alectryon@tango@medium@aluminium]}
@@ -199,7 +199,7 @@
 \alectryon@newenvironment{conclusion}{\alectryon@strut{}\alectryon@raggedright}{\par}
   {}
 
-\newcommand*{\alectryon@hrefmarker}[1]
+\newcommand*{\alectryon@mrefmarker}[1]
   {\alectryon@nobreakspace%
    {\setlength{\fboxsep}{1pt}\fbox{\footnotesize\textbf{#1}}}}
 
@@ -223,8 +223,8 @@
    \alectryon@copyenvironment{messages}
    \alectryon@copyenvironment{message}
    \alectryon@copyenvironment{conclusion}
-   \alectryon@copymacro{hreflabel}
-   \alectryon@copymacro{hrefmarker}
+   \alectryon@copymacro{anchor}
+   \alectryon@copymacro{mrefmarker}
    \alectryon@copymacro{infrule}
    \alectryon@copymacro{gid}
    \alectryon@copymacro{hypn}

alectryon/docutils.py

@@ -98,7 +98,7 @@ class alectryon_pending(nodes.pending):
 class alectryon_pending_toggle(nodes.pending):
     pass
 
-class alectryon_pending_href(nodes.pending):
+class alectryon_pending_mref(nodes.pending):
     pass
 
 class alectryon_pending_io(nodes.pending):
@@ -338,14 +338,14 @@ def next(self, style):
         num = self.counters[style] = self.counters[style] + 1
         return style.fmt(num)
 
-class HrefError(ValueError):
+class MrefError(ValueError):
     pass
 
-class AlectryonHrefTransform(OneTimeTransform):
+class AlectryonMrefTransform(OneTimeTransform):
     """Convert Alectryon input/output pairs into HTML or LaTeX.
 
     This transform is triggered by a ``pending`` node added by
-    the ``:href:`` role.
+    the ``:mref:`` role.
     """
     default_priority = 995
 
@@ -363,14 +363,14 @@ def _find_sentence(fragments, needle):
             if isinstance(fr, RichSentence) and needle in fr.contents:
                 return fr
         # LATER: Add a way to name sentences to make them easier to select
-        raise HrefError("No sentence matches '{}'".format(needle))
+        raise MrefError("No sentence matches '{}'".format(needle))
 
     @staticmethod
     def _find_named(kind, items, needle):
         for item in items:
             if needle in getattr(item, "names", [getattr(item, "name", None)]):
                 return item
-        raise HrefError("No such {}: '{}'".format(kind, needle))
+        raise MrefError("No such {}: '{}'".format(kind, needle))
 
     @classmethod
     def _find_goal(cls, goals, needle):
@@ -388,16 +388,16 @@ def _find_hyp(cls, hyps, name, needle):
         for h in hyps:
             if needle in h.type or (h.body and needle in h.body):
                 return h
-        raise HrefError("No hypothesis matches '{}'".format(needle))
+        raise MrefError("No hypothesis matches '{}'".format(needle))
 
     @classmethod
-    def _find_href_target(cls, node, ios, last_io):
+    def _find_mref_target(cls, node, ios, last_io):
         query = node.details["query"]
 
         root = query.get("root")
         io = ios.get(root) if root else last_io
         if io is None:
-            raise HrefError("Reference to unknown Alectryon block")
+            raise MrefError("Reference to unknown Alectryon block")
 
         sentence = cls._find_sentence(io.details["fragments"], query["sentence"])
         goals = [g for gs in transforms.fragment_goal_sets(sentence) for g in gs]
@@ -414,8 +414,8 @@ def _find_href_target(cls, node, ios, last_io):
                 return goal
         return sentence
 
-    def replace_one_href(self, gensym, refcounter, node, ios, last_io):
-        target = self._find_href_target(node, ios, last_io)
+    def replace_one_mref(self, gensym, refcounter, node, ios, last_io):
+        target = self._find_mref_target(node, ios, last_io)
         if not target.ids:
             target_id = nodes.make_id(node.details["target"])
             target.ids.append(gensym(target_id))
@@ -426,21 +426,21 @@ def replace_one_href(self, gensym, refcounter, node, ios, last_io):
         marker, refid = target.markers[-1], target.ids[-1]
         ref = nodes.reference(node.rawsource, marker, classes=[], refid=refid)
         node.replace_self(ref)
-        ref["classes"].append("alectryon-href")
+        ref["classes"].append("alectryon-mref")
 
     def _apply(self, **_kwargs):
         ios = {id: node
                for node in self.document.traverse(alectryon_pending_io)
                for id in node.get("ids", ())}
         refcounter, gensym = RefCounter(), Gensym(_gensym_stem(self.document, "-"))
-        io_or_href = lambda n: isinstance(n, (alectryon_pending_io, alectryon_pending_href))
-        for node in self.document.traverse(io_or_href):
+        io_or_mref = lambda n: isinstance(n, (alectryon_pending_io, alectryon_pending_mref))
+        for node in self.document.traverse(io_or_mref):
             if isinstance(node, alectryon_pending_io):
                 last_io = node
-            elif isinstance(node, alectryon_pending_href):
+            elif isinstance(node, alectryon_pending_mref):
                 try:
-                    self.replace_one_href(gensym, refcounter, node, ios, last_io)
-                except HrefError as e:
+                    self.replace_one_mref(gensym, refcounter, node, ios, last_io)
+                except MrefError as e:
                     msg = "Error in '{}': {}".format(node.rawsource, e)
                     self._warn(node, msg)
 
@@ -686,15 +686,15 @@ def coq_id_role(# pylint: disable=dangerous-default-value,unused-argument
 }
 DEFAULT_COUNTER_STYLE = CounterStyle.of_str(COUNTER_STYLES['decimal'])
 
-def highlight_ref_role(# pylint: disable=dangerous-default-value,unused-argument
+def marker_ref_role(# pylint: disable=dangerous-default-value,unused-argument
         role, rawtext, text, lineno, inliner, options={}, content=[]):
     title, target = _parse_ref(text)
     if target is None:
         title, target = None, title
 
     m = HIGHLIGHT_REF_TARGET_RE.match(target)
     if target[0] in "#." and not m:
-        MSG = "Cannot parse ``:href:`` target ``{}``.".format(target)
+        MSG = "Cannot parse ``:mref:`` target ``{}``.".format(target)
         msg = inliner.reporter.error(MSG, line=lineno)
         return [inliner.problematic(rawtext, rawtext, msg)], [msg]
 
@@ -705,8 +705,8 @@ def highlight_ref_role(# pylint: disable=dangerous-default-value,unused-argument
                "counter-style": cs }
 
     roles.set_classes(options)
-    node = alectryon_pending_href(
-        AlectryonHrefTransform, details, rawtext, **options)
+    node = alectryon_pending_mref(
+        AlectryonMrefTransform, details, rawtext, **options)
     set_line(node, lineno, inliner.reporter)
     inliner.document.note_pending(node)
     return [node], []
@@ -716,8 +716,8 @@ def _opt_counter_style(arg):
         arg = COUNTER_STYLES[directives.choice(arg, list(COUNTER_STYLES))]
     return CounterStyle.of_str(arg)
 
-highlight_ref_role.name = "href"
-highlight_ref_role.options = {
+marker_ref_role.name = "mref"
+marker_ref_role.options = {
     'counter-style': _opt_counter_style
 }
 
@@ -992,12 +992,12 @@ def get_pipeline(frontend, backend, dialect):
          alectryon_pending_io]
 TRANSFORMS = [ActivateMathJaxTransform,
               AlectryonTransform,
-              AlectryonHrefTransform,
+              AlectryonMrefTransform,
               AlectryonPostTransform]
 DIRECTIVES = [CoqDirective,
               AlectryonToggleDirective,
               ExperimentalExerciseDirective]
-ROLES = [alectryon_bubble, coq_code_role, coq_id_role, highlight_ref_role]
+ROLES = [alectryon_bubble, coq_code_role, coq_id_role, marker_ref_role]
 
 def register():
     """Tell Docutils about our roles and directives."""

alectryon/html.py

@@ -110,7 +110,7 @@ def gen_hyp(self, hyp):
                 with tags.span(cls="hyp-type"):
                     tags.b(":")
                     tags.span(self.highlight(hyp.type))
-            self.gen_hrefs(hyp)
+            self.gen_mrefs(hyp)
 
     @deduplicate(".goal-hyps")
     def gen_hyps(self, hyps):
@@ -121,7 +121,7 @@ def gen_hyps(self, hyps):
     @deduplicate(".goal-conclusion")
     def gen_ccl(self, conclusion):
         with tags.div(self.highlight(conclusion.contents), cls="goal-conclusion"):
-            self.gen_hrefs(conclusion)
+            self.gen_mrefs(conclusion)
 
     @deduplicate(".alectryon-goal")
     def gen_goal(self, goal, toggle=None):
@@ -139,7 +139,7 @@ def gen_goal(self, goal, toggle=None):
                 tags.hr()
                 if goal.name:
                     tags.span(goal.name, cls="goal-name")
-                self.gen_href_markers(goal.markers)
+                self.gen_mref_markers(goal.markers)
             self.gen_ccl(goal.conclusion)
 
     def gen_checkbox(self, checked, cls):
@@ -169,12 +169,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.contents)):
-            self.gen_hrefs(fr)
+            self.gen_mrefs(fr)
 
     def gen_message(self, message):
         with tags.blockquote(self.highlight(message.contents),
                              cls="alectryon-message"):
-            self.gen_hrefs(message)
+            self.gen_mrefs(message)
 
     @deduplicate(".alectryon-output")
     def gen_output(self, fr):
@@ -224,14 +224,14 @@ def gen_ids(ids):
             tags.span(id=name) # FIXME insert at beg of parent
 
     @classmethod
-    def gen_hrefs(cls, nt):
+    def gen_mrefs(cls, nt):
         cls.gen_ids(nt.ids)
-        cls.gen_href_markers(nt.markers)
+        cls.gen_mref_markers(nt.markers)
 
     @staticmethod
-    def gen_href_markers(markers):
+    def gen_mref_markers(markers):
         for marker in markers:
-            tags.span(marker, cls="alectryon-href-marker")
+            tags.span(marker, cls="alectryon-mref-marker")
 
     def gen_fragments(self, fragments, ids=(), classes=()):
         """Serialize a list of `fragments` to HTML."""

alectryon/latex.py

@@ -180,7 +180,7 @@ def gen_hyp(self, hyp):
         hbody = self.highlight(hyp.body) if hyp.body else []
         with macros.hyp(args=[names], optargs=hbody, verbatim=True):
             self.highlight(hyp.type)
-            self.gen_hrefs(hyp)
+            self.gen_mrefs(hyp)
 
     def gen_goal(self, goal):
         """Serialize a goal to LaTeX."""
@@ -192,10 +192,10 @@ def gen_goal(self, goal):
             with macros.infrule():
                 if goal.name:
                     macros.gid(goal.name)
-                self.gen_href_markers(goal.markers)
+                self.gen_mref_markers(goal.markers)
             with environments.conclusion(verbatim=True):
                 self.highlight(goal.conclusion.contents)
-                self.gen_hrefs(goal.conclusion)
+                self.gen_mrefs(goal.conclusion)
 
     def gen_goals(self, first, more):
         self.gen_goal(first)
@@ -222,12 +222,12 @@ def gen_input(self, fr):
             # middle of a line.
             if not fr.outputs:
                 self.gen_whitespace(fr.suffixes)
-            self.gen_hrefs(fr)
+            self.gen_mrefs(fr)
 
     def gen_message(self, msg):
         with environments.message(verbatim=True):
             self.highlight(msg.contents)
-            self.gen_hrefs(msg)
+            self.gen_mrefs(msg)
 
     def gen_output(self, fr):
         with environments.output():
@@ -260,17 +260,17 @@ def gen_fragment(self, fr):
     @staticmethod
     def gen_ids(ids):
         for name in ids:
-            macros.hreflabel(Raw(name)) # FIXME insert at beginning of parent
+            macros.anchor(Raw(name)) # FIXME insert at beginning of parent
 
     @classmethod
-    def gen_hrefs(cls, nt):
+    def gen_mrefs(cls, nt):
         cls.gen_ids(nt.ids)
-        cls.gen_href_markers(nt.markers)
+        cls.gen_mref_markers(nt.markers)
 
     @staticmethod
-    def gen_href_markers(markers):
+    def gen_mref_markers(markers):
         for marker in markers:
-            macros.hrefmarker(Raw(marker))
+            macros.mrefmarker(Raw(marker))
 
     def gen_fragments(self, fragments, ids=(), classes=()): # pylint: disable=unused-argument
         """Serialize a list of `fragments` to LaTeX."""