Skip to content

Commit 72749bd

Browse files
cpitclaudelcpitclaudel
committed
docutils, cli: Fix inline code highlighting
Inline code samples were generating long Pygments class names, while code blocks were using a short class names (and hence leveraging tango_subtle).
1 parent d3e655a commit 72749bd

File tree

4 files changed

+11
-6
lines changed

4 files changed

+11
-6
lines changed

‎alectryon/cli.py‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,6 @@ def _gen_docutils(source, fpath,
9191

9292
settings_overrides = {
9393
'traceback': True,
94-
'embed_stylesheet': False,
9594
'stylesheet_path': None,
9695
'input_encoding': 'utf-8',
9796
'output_encoding': 'utf-8',

‎alectryon/docutils.py‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -603,7 +603,6 @@ class Translator(base):
603603
' xml:lang="%(lang)s" lang="%(lang)s">\n<head>\n'
604604

605605
def __init__(self, document):
606-
document.settings.syntax_highlight = "short"
607606
document.settings.math_output = "MathJax " + self.MATHJAX_URL
608607
super().__init__(document)
609608

@@ -655,6 +654,13 @@ class Writer(base):
655654
('Alectryon HTML writer options',
656655
None, ALECTRYON_SETTINGS))
657656

657+
settings_default_overrides = { # By default:
658+
# We embed the short-classes Pygments stylesheet, not the long-classes one…
659+
"syntax_highlight": "short",
660+
# … and we want to link to Alectryon's stylesheet, not embed it
661+
"embed_stylesheet": False,
662+
}
663+
658664
def __init__(self, *args, **kwargs):
659665
super().__init__(*args, **kwargs)
660666
self.translator_class = translator

‎recipes/output/document.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ <h1>Strengthening the spec</h1>
7777
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre></div>
7878
<div class="section" id="writing-a-fixpoint">
7979
<h1>Writing a fixpoint</h1>
80-
<p>But writing a fixpoint (either with the <code class="highlight coq"><span class="keyword namespace">Fixpoint</span></code> command or with the <code class="highlight coq"><span class="keyword reserved">fix</span></code> tactic) is much nicer:</p>
80+
<p>But writing a fixpoint (either with the <code class="highlight coq"><span class="kn">Fixpoint</span></code> command or with the <code class="highlight coq"><span class="kr">fix</span></code> tactic) is much nicer:</p>
8181
<pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="document-v-rst-chk1c" style="display: none" type="checkbox"><label class="alectryon-input" for="document-v-rst-chk1c"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">even_Even_fp</span> (<span class="nv">n</span>: nat):
8282
even n = true &lt;-&gt; Even n.</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>even_Even_fp</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : nat,
8383
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">even n = true &lt;-&gt; Even n</span></div></blockquote></div></div></small><span class="alectryon-wsp">
@@ -102,7 +102,7 @@ <h1>Writing a fixpoint</h1>
102102
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">even n = true -&gt; Even (S (S n))</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">apply</span> even_Even_fp; <span class="bp">assumption</span>.</span></span><span class="alectryon-wsp">
103103
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="document-v-rst-chk27" style="display: none" type="checkbox"><label class="alectryon-input" for="document-v-rst-chk27"><span class="highlight">+</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>even_Even_fp</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : nat,
104104
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Even (S (S n)) -&gt; even n = true</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="nb">inversion</span> <span class="mi">1</span>; <span class="nb">apply</span> even_Even_fp; <span class="bp">assumption</span>.</span></span><span class="alectryon-wsp">
105-
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><p>Note that the standard library already contains a <a class="mycoqid reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">boolean</a> <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">predicate</a> for <code class="highlight coq"><span class="name">even</span></code> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">Coq.Init.Nat.even</a>, or <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">even</a> for short), as well as an <a class="mycoqid reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">inductive one</a> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">Nat.Even</a> in module <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#">Coq.Arith.PeanoNat</a>).</p>
105+
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><p>Note that the standard library already contains a <a class="mycoqid reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">boolean</a> <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">predicate</a> for <code class="highlight coq"><span class="n">even</span></code> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">Coq.Init.Nat.even</a>, or <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">even</a> for short), as well as an <a class="mycoqid reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">inductive one</a> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">Nat.Even</a> in module <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#">Coq.Arith.PeanoNat</a>).</p>
106106
</div>
107107
</div>
108108
</div></body>

‎recipes/output/literate.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ <h1>Strengthening the spec</h1>
7777
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre></div>
7878
<div class="section" id="writing-a-fixpoint">
7979
<h1>Writing a fixpoint</h1>
80-
<p>But writing a fixpoint (either with the <code class="highlight coq"><span class="keyword namespace">Fixpoint</span></code> command or with the <code class="highlight coq"><span class="keyword reserved">fix</span></code> tactic) is much nicer:</p>
80+
<p>But writing a fixpoint (either with the <code class="highlight coq"><span class="kn">Fixpoint</span></code> command or with the <code class="highlight coq"><span class="kr">fix</span></code> tactic) is much nicer:</p>
8181
<pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="literate-v-chk1c" style="display: none" type="checkbox"><label class="alectryon-input" for="literate-v-chk1c"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">even_Even_fp</span> (<span class="nv">n</span>: nat):
8282
even n = true &lt;-&gt; Even n.</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>even_Even_fp</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : nat,
8383
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">even n = true &lt;-&gt; Even n</span></div></blockquote></div></div></small><span class="alectryon-wsp">
@@ -102,7 +102,7 @@ <h1>Writing a fixpoint</h1>
102102
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">even n = true -&gt; Even (S (S n))</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="nb">constructor</span>; <span class="nb">apply</span> even_Even_fp; <span class="bp">assumption</span>.</span></span><span class="alectryon-wsp">
103103
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="literate-v-chk27" style="display: none" type="checkbox"><label class="alectryon-input" for="literate-v-chk27"><span class="highlight">+</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>even_Even_fp</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="kr">forall</span> <span class="nv">n</span> : nat,
104104
even n = true &lt;-&gt; Even n</span></span></div><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Even (S (S n)) -&gt; even n = true</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="nb">inversion</span> <span class="mi">1</span>; <span class="nb">apply</span> even_Even_fp; <span class="bp">assumption</span>.</span></span><span class="alectryon-wsp">
105-
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><p>Note that the standard library already contains a <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">boolean</a> <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">predicate</a> for <code class="highlight coq"><span class="name">even</span></code> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">Coq.Init.Nat.even</a>, or <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">even</a> for short), as well as an <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">inductive one</a> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">Nat.Even</a> in module <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#">Coq.Arith.PeanoNat</a>).</p>
105+
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><p>Note that the standard library already contains a <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">boolean</a> <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">predicate</a> for <code class="highlight coq"><span class="n">even</span></code> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">Coq.Init.Nat.even</a>, or <a class="reference external" href="https://coq.inria.fr/library/Coq.Init.Nat.html#even">even</a> for short), as well as an <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">inductive one</a> (called <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#Nat.Even">Nat.Even</a> in module <a class="reference external" href="https://coq.inria.fr/library/Coq.Arith.PeanoNat.html#">Coq.Arith.PeanoNat</a>).</p>
106106
</div>
107107
</div>
108108
</div></body>

0 commit comments

Comments
 (0)