[doc] Move the LaTeX preamble to a separate .tex file

4 files changed, 134 insertions, 118 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 983f4e665f..ab4648d577 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -274,14 +274,12 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           -----------------------------
           \WTEG{\forall~x:T,U}{\Prop}
 
-``.. preamble::`` A reST directive for hidden math.
-    Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s.
+``.. preamble::`` A reST directive to include a TeX file.
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
 
-    Example::
-
-       .. preamble::
+    Usage::
 
-          \newcommand{\paren}[#1]{\left(#1\right)}
+       .. preamble:: preamble.tex
 
 Coq roles
 =========
diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst
index 395f558a85..dcbc3322ac 100644
--- a/doc/sphinx/preamble.rst
+++ b/doc/sphinx/preamble.rst
@@ -1,92 +1,6 @@
-.. preamble::
+.. only:: html
 
-   \[
-   \newcommand{\alors}{\textsf{then}}
-   \newcommand{\alter}{\textsf{alter}}
-   \newcommand{\as}{\kw{as}}
-   \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
-   \newcommand{\bool}{\textsf{bool}}
-   \newcommand{\case}{\kw{case}}
-   \newcommand{\conc}{\textsf{conc}}
-   \newcommand{\cons}{\textsf{cons}}
-   \newcommand{\consf}{\textsf{consf}}
-   \newcommand{\conshl}{\textsf{cons\_hl}}
-   \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
-   \newcommand{\emptyf}{\textsf{emptyf}}
-   \newcommand{\End}{\kw{End}}
-   \newcommand{\endkw}{\kw{end}}
-   \newcommand{\EqSt}{\textsf{EqSt}}
-   \newcommand{\even}{\textsf{even}}
-   \newcommand{\evenO}{\textsf{even_O}}
-   \newcommand{\evenS}{\textsf{even_S}}
-   \newcommand{\false}{\textsf{false}}
-   \newcommand{\filter}{\textsf{filter}}
-   \newcommand{\Fix}{\kw{Fix}}
-   \newcommand{\fix}{\kw{fix}}
-   \newcommand{\for}{\textsf{for}}
-   \newcommand{\forest}{\textsf{forest}}
-   \newcommand{\from}{\textsf{from}}
-   \newcommand{\Functor}{\kw{Functor}}
-   \newcommand{\haslength}{\textsf{has\_length}}
-   \newcommand{\hd}{\textsf{hd}}
-   \newcommand{\ident}{\textsf{ident}}
-   \newcommand{\In}{\kw{in}}
-   \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
-   \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
-   \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
-   \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
-   \newcommand{\injective}{\kw{injective}}
-   \newcommand{\kw}[1]{\textsf{#1}}
-   \newcommand{\lb}{\lambda}
-   \newcommand{\length}{\textsf{length}}
-   \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
-   \newcommand{\List}{\textsf{list}}
-   \newcommand{\lra}{\longrightarrow}
-   \newcommand{\Match}{\kw{match}}
-   \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
-   \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
-   \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
-   \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
-   \newcommand{\mto}{.\;}
-   \newcommand{\Nat}{\mathbb{N}}
-   \newcommand{\nat}{\textsf{nat}}
-   \newcommand{\Nil}{\textsf{nil}}
-   \newcommand{\nilhl}{\textsf{nil\_hl}}
-   \newcommand{\nO}{\textsf{O}}
-   \newcommand{\node}{\textsf{node}}
-   \newcommand{\nS}{\textsf{S}}
-   \newcommand{\odd}{\textsf{odd}}
-   \newcommand{\oddS}{\textsf{odd_S}}
-   \newcommand{\ovl}[1]{\overline{#1}}
-   \newcommand{\Pair}{\textsf{pair}}
-   \newcommand{\Prod}{\textsf{prod}}
-   \newcommand{\Prop}{\textsf{Prop}}
-   \newcommand{\return}{\kw{return}}
-   \newcommand{\Set}{\textsf{Set}}
-   \newcommand{\si}{\textsf{if}}
-   \newcommand{\sinon}{\textsf{else}}
-   \newcommand{\Sort}{\cal S}
-   \newcommand{\Str}{\textsf{Stream}}
-   \newcommand{\Struct}{\kw{Struct}}
-   \newcommand{\subst}[3]{#1\{#2/#3\}}
-   \newcommand{\tl}{\textsf{tl}}
-   \newcommand{\tree}{\textsf{tree}}
-   \newcommand{\true}{\textsf{true}}
-   \newcommand{\Type}{\textsf{Type}}
-   \newcommand{\unfold}{\textsf{unfold}}
-   \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
-   \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
-   \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
-   \newcommand{\WFE}[1]{\WF{E}{#1}}
-   \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
-   \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
-   \newcommand{\with}{\kw{with}}
-   \newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
-   \newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
-   \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
-   \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
-   \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
-   \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
-   \newcommand{\zeroone}[1]{[{#1}]}
-   \newcommand{\zeros}{\textsf{zeros}}
-   \]
+   .. This is included once per page in the HTML build, and a single time (in the
+      document's preamble) in the LaTeX one.
+
+   .. preamble:: /preamble.tex
diff --git a/doc/sphinx/preamble.tex b/doc/sphinx/preamble.tex
new file mode 100644
index 0000000000..b4fc608e47
--- /dev/null
+++ b/doc/sphinx/preamble.tex
@@ -0,0 +1,88 @@
+\newcommand{\alors}{\textsf{then}}
+\newcommand{\alter}{\textsf{alter}}
+\newcommand{\as}{\kw{as}}
+\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
+\newcommand{\bool}{\textsf{bool}}
+\newcommand{\case}{\kw{case}}
+\newcommand{\conc}{\textsf{conc}}
+\newcommand{\cons}{\textsf{cons}}
+\newcommand{\consf}{\textsf{consf}}
+\newcommand{\conshl}{\textsf{cons\_hl}}
+\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
+\newcommand{\emptyf}{\textsf{emptyf}}
+\newcommand{\End}{\kw{End}}
+\newcommand{\kwend}{\kw{end}}
+\newcommand{\EqSt}{\textsf{EqSt}}
+\newcommand{\even}{\textsf{even}}
+\newcommand{\evenO}{\textsf{even}_\textsf{O}}
+\newcommand{\evenS}{\textsf{even}_\textsf{S}}
+\newcommand{\false}{\textsf{false}}
+\newcommand{\filter}{\textsf{filter}}
+\newcommand{\Fix}{\kw{Fix}}
+\newcommand{\fix}{\kw{fix}}
+\newcommand{\for}{\textsf{for}}
+\newcommand{\forest}{\textsf{forest}}
+\newcommand{\from}{\textsf{from}}
+\newcommand{\Functor}{\kw{Functor}}
+\newcommand{\haslength}{\textsf{has\_length}}
+\newcommand{\hd}{\textsf{hd}}
+\newcommand{\ident}{\textsf{ident}}
+\newcommand{\In}{\kw{in}}
+\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
+\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
+\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
+\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
+\newcommand{\injective}{\kw{injective}}
+\newcommand{\kw}[1]{\textsf{#1}}
+\newcommand{\lb}{\lambda}
+\newcommand{\length}{\textsf{length}}
+\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
+\newcommand{\List}{\textsf{list}}
+\newcommand{\lra}{\longrightarrow}
+\newcommand{\Match}{\kw{match}}
+\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
+\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
+\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
+\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
+\newcommand{\mto}{.\;}
+\newcommand{\Nat}{\mathbb{N}}
+\newcommand{\nat}{\textsf{nat}}
+\newcommand{\Nil}{\textsf{nil}}
+\newcommand{\nilhl}{\textsf{nil\_hl}}
+\newcommand{\nO}{\textsf{O}}
+\newcommand{\node}{\textsf{node}}
+\newcommand{\nS}{\textsf{S}}
+\newcommand{\odd}{\textsf{odd}}
+\newcommand{\oddS}{\textsf{odd}_\textsf{S}}
+\newcommand{\ovl}[1]{\overline{#1}}
+\newcommand{\Pair}{\textsf{pair}}
+\newcommand{\Prod}{\textsf{prod}}
+\newcommand{\Prop}{\textsf{Prop}}
+\newcommand{\return}{\kw{return}}
+\newcommand{\Set}{\textsf{Set}}
+\newcommand{\si}{\textsf{if}}
+\newcommand{\sinon}{\textsf{else}}
+\newcommand{\Sort}{\cal S}
+\newcommand{\Str}{\textsf{Stream}}
+\newcommand{\Struct}{\kw{Struct}}
+\newcommand{\subst}[3]{#1\{#2/#3\}}
+\newcommand{\tl}{\textsf{tl}}
+\newcommand{\tree}{\textsf{tree}}
+\newcommand{\true}{\textsf{true}}
+\newcommand{\Type}{\textsf{Type}}
+\newcommand{\unfold}{\textsf{unfold}}
+\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
+\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
+\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
+\newcommand{\WFE}[1]{\WF{E}{#1}}
+\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
+\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
+\newcommand{\with}{\kw{with}}
+\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
+\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
+\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
+\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
+\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
+\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
+\newcommand{\zeroone}[1]{[{#1}]}
+\newcommand{\zeros}{\textsf{zeros}}
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index d81355e865..b3641c152b 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -34,7 +34,7 @@ from sphinx.util.logging import getLogger
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
 from sphinx.domains.std import token_xrefs
-from sphinx.ext.mathbase import MathDirective, displaymath
+from sphinx.ext import mathbase
 
 from . import coqdoc
 from .repl import ansicolors
@@ -58,6 +58,15 @@ def make_target(objtype, targetid):
     """Create a target to an object of type objtype and id targetid"""
     return "coq:{}.{}".format(objtype, targetid)
 
+def make_math_node(latex, docname, nowrap):
+    node = mathbase.displaymath()
+    node['latex'] = latex
+    node['label'] = None # Otherwise equations are numbered
+    node['nowrap'] = nowrap
+    node['docname'] = docname
+    node['number'] = None
+    return node
+
 class CoqObject(ObjectDescription):
     """A generic Coq object for Sphinx; all Coq objects are subclasses of this.
 
@@ -602,24 +611,39 @@ class ExampleDirective(BaseAdmonition):
         self.options['classes'] = ['admonition', 'note']
         return super().run()
 
-class PreambleDirective(MathDirective):
-    r"""A reST directive for hidden math.
+class PreambleDirective(Directive):
+    r"""A reST directive to include a TeX file.
 
-    Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s.
-
-    Example::
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
 
-       .. preamble::
+    Usage::
 
-          \newcommand{\paren}[#1]{\left(#1\right)}
+       .. preamble:: preamble.tex
     """
 
-    directive_name = "preamble"
+    has_content = False
+    required_arguments = 1
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = {}
 
     def run(self):
-        self.options['nowrap'] = True
-        [node] = super().run()
+        document = self.state.document
+        env = document.settings.env
+
+        if not document.settings.file_insertion_enabled:
+            msg = 'File insertion disabled'
+            return [document.reporter.warning(msg, line=self.lineno)]
+
+        rel_fname, abs_fname = env.relfn2path(self.arguments[0])
+        env.note_dependency(rel_fname)
+
+        with open(abs_fname, encoding="utf-8") as ltx:
+            latex = ltx.read()
+
+        node = make_math_node(latex, env.docname, nowrap=True)
         node['classes'] = ["math-preamble"]
+        set_source_info(self, node)
         return [node]
 
 class InferenceDirective(Directive):
@@ -652,15 +676,6 @@ class InferenceDirective(Directive):
     final_argument_whitespace = True
     directive_name = "inference"
 
-    def make_math_node(self, latex):
-        node = displaymath()
-        node['latex'] = latex
-        node['label'] = None # Otherwise equations are numbered
-        node['nowrap'] = False
-        node['docname'] = self.state.document.settings.env.docname
-        node['number'] = None
-        return node
-
     @staticmethod
     def prepare_latex_operand(op):
         # TODO: Could use a fancier inference class in LaTeX
@@ -680,7 +695,8 @@ class InferenceDirective(Directive):
         title = self.arguments[0]
         content = '\n'.join(self.content)
         latex = self.prepare_latex(content)
-        math_node = self.make_math_node(latex)
+        docname = self.state.document.settings.env.docname
+        math_node = make_math_node(latex, docname, nowrap=False)
 
         tid = nodes.make_id(title)
         target = nodes.target('', '', ids=['inference-' + tid])