html, css: Use simpler markup for hypotheses

Part of GH-35.  This saves quite a bit of space.

Author: cpitclaudel

alectryon/assets/alectryon.css

@@ -312,7 +312,7 @@ In any case, make an exception for comments:
 .alectryon-io .alectryon-message,
 .alectryon-io .alectryon-goals,
 .alectryon-io .alectryon-goal,
-.alectryon-io .goal-hyp,
+.alectryon-io .goal-hyps > div,
 .alectryon-io .goal-conclusion {
     border-radius: 0.15em;
 }
@@ -343,33 +343,34 @@ In any case, make an exception for comments:
     padding-bottom: 0.5em;
 }
 
-.alectryon-io .goal-hyp,
+.alectryon-io .goal-hyps > div,
 .alectryon-io .goal-conclusion {
     background: #eeeeec;
     display: inline-block;
     padding: 0.15em 0.35em;
 }
 
-.alectryon-io .goal-hyp {
+.alectryon-io .goal-hyps > div {
     align-items: baseline;
     display: inline-flex;
     margin: 0.15em 0.25em;
 }
 
-.alectryon-io .hyp-names {
+.alectryon-io .goal-hyps > div > var {
     font-weight: 600;
+    font-style: unset;
     /* Shrink the list of names, but let it grow as long as space is available. */
     flex-basis: min-content;
     flex-grow: 1;
 }
 
-.alectryon-io .hyp-punct {
+.alectryon-io .goal-hyps > div b {
     font-weight: 600;
     margin: 0 0.5em;
 }
 
-.alectryon-io .hyp-body-block,
-.alectryon-io .hyp-type-block {
+.alectryon-io .hyp-body,
+.alectryon-io .hyp-type {
     display: flex;
     align-items: baseline;
 }

alectryon/html.py

@@ -83,18 +83,16 @@ def gen_label(toggle, cls, *contents):
     def gen_hyps(self, hyps):
         with tags.div(cls="goal-hyps"):
             for hyp in hyps:
-                with tags.div(cls="goal-hyp"):
-                    tags.span(", ".join(hyp.names), cls="hyp-names")
-                    with tags.span():
+                with tags.div():
+                    tags.var(", ".join(hyp.names))
+                    with tags.span(): # For alignment
                         if hyp.body:
-                            with tags.span(cls="hyp-body-block"):
-                                tags.span(":=", cls="hyp-punct")
-                                with tags.span(cls="hyp-body"):
-                                    self.highlight(hyp.body)
-                        with tags.span(cls="hyp-type-block"):
-                            tags.span(":", cls="hyp-punct")
-                            with tags.span(cls="hyp-type"):
-                                self.highlight(hyp.type)
+                            with tags.span(cls="hyp-body"):
+                                tags.b(":=")
+                                self.highlight(hyp.body)
+                        with tags.span(cls="hyp-type"):
+                            tags.b(":")
+                            self.highlight(hyp.type)
 
     def gen_goal(self, goal, toggle=None):
         """Serialize a goal to HTML."""

recipes/mathjax.rst

@@ -61,12 +61,11 @@ Then we set up MathJax to render the proofs properly (look at the page source to
    <script type="text/javascript">
      function addMathDelimiters() {
         // 1. Find all relevant Alectryon tags
-        var spans = document.querySelectorAll(".goal-conclusion .highlight, .goal-hyp .highlight");
+        var spans = document.querySelectorAll(".goal-conclusion .highlight, .goal-hyps > div .highlight");
 
         // 2. Wrap the contents of each in \(\) math delimiters
         spans.forEach(function (e) {
-            var math = document.createTextNode('\\[' + e.innerText + '\\]');
-            e.parentNode.replaceChild(math, e);
+            e.innerText = '\\[' + e.innerText + '\\]';
         });
      }
 
@@ -86,7 +85,7 @@ Then we set up MathJax to render the proofs properly (look at the page source to
    </script>
 
    <style type="text/css"> /* Override MathJax margins */
-       .hyp-type > *, .goal-conclusion > * {
+       .goal-conclusion .highlight > *, .goal-hyps > div .highlight > * {
            margin: 0 !important;
        }
    </style>

recipes/output/mathjax.html

@@ -58,12 +58,11 @@ <h1 class="title">Using MathJax with Alectryon</h1>
 <script type="text/javascript">
   function addMathDelimiters() {
      // 1. Find all relevant Alectryon tags
-     var spans = document.querySelectorAll(".goal-conclusion .highlight, .goal-hyp .highlight");
+     var spans = document.querySelectorAll(".goal-conclusion .highlight, .goal-hyps > div .highlight");
 
      // 2. Wrap the contents of each in \(\) math delimiters
      spans.forEach(function (e) {
-         var math = document.createTextNode('\\[' + e.innerText + '\\]');
-         e.parentNode.replaceChild(math, e);
+         e.innerText = '\\[' + e.innerText + '\\]';
      });
   }
 
@@ -83,7 +82,7 @@ <h1 class="title">Using MathJax with Alectryon</h1>
 </script>
 
 <style type="text/css"> /* Override MathJax margins */
-    .hyp-type > *, .goal-conclusion > * {
+    .goal-conclusion .highlight > *, .goal-hyps > div .highlight > * {
         margin: 0 !important;
     }
 </style><p>And finally we write the actual proofs:</p>