diff options
Diffstat (limited to 'doc/sphinx/_static')
| -rw-r--r-- | doc/sphinx/_static/ansi-dark.css | 4 | ||||
| -rw-r--r-- | doc/sphinx/_static/ansi.css | 4 | ||||
| -rw-r--r-- | doc/sphinx/_static/coqdoc.css | 4 | ||||
| -rw-r--r-- | doc/sphinx/_static/coqnotations.sty | 17 | ||||
| -rw-r--r-- | doc/sphinx/_static/notations.css | 58 | ||||
| -rw-r--r-- | doc/sphinx/_static/notations.js | 4 | ||||
| -rw-r--r-- | doc/sphinx/_static/pre-text.css | 4 |
7 files changed, 77 insertions, 18 deletions
diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css index bbace7c553..f02f522bdd 100644 --- a/doc/sphinx/_static/ansi-dark.css +++ b/doc/sphinx/_static/ansi-dark.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index b3b5341166..2a618f68d2 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css index 7a3d59d4c0..32cb0a7a15 100644 --- a/doc/sphinx/_static/coqdoc.css +++ b/doc/sphinx/_static/coqdoc.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 3548b8754c..3dfe4db439 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -67,11 +67,26 @@ \newcssclass{notation-sup}{\nsup{#1}} \newcssclass{notation-sub}{\nsub{#1}} -\newcssclass{notation}{\nnotation{#1}} +\newcssclass{notation}{\nnotation{\textbf{#1}}} \newcssclass{repeat}{\nrepeat{#1}} \newcssclass{repeat-wrapper}{\nwrapper{#1}} +\newcssclass{repeat-wrapper-with-sub}{\nwrapper{#1}} \newcssclass{hole}{\nhole{#1}} \newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}} \newcssclass{alternative-block}{#1} \newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}} \newcssclass{alternative-separator}{\quad\naltsep{}\quad} +\newcssclass{prodn-table}{% + \begin{savenotes} + \sphinxattablestart + \begin{tabulary}{\linewidth}[t]{lLL} + #1 + \end{tabulary} + \par + \sphinxattableend + \end{savenotes}} +% latex puts targets 1 line below where they should be; prodn-target corrects for this +\newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}} +\newcssclass{prodn-cell-nonterminal}{#1 &} +\newcssclass{prodn-cell-op}{#1 &} +\newcssclass{prodn-cell-production}{#1\\} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 4a5fa0b328..733a73bd21 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ @@ -10,6 +10,7 @@ .notation { /* font-family: "Ubuntu Mono", "Consolas", monospace; */ white-space: pre-wrap; + font-weight: bold; } .notation .notation-sup { @@ -85,7 +86,8 @@ padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ } -.notation .repeat-wrapper { +.notation .repeat-wrapper, +.notation .repeat-wrapper-with-sub { display: inline-block; position: relative; margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */ @@ -165,10 +167,52 @@ /* Overrides */ /*************/ -.rst-content table.docutils td, .rst-content table.docutils th { - padding: 8px; /* Reduce horizontal padding */ - border-left: none; - border-right: none; +.prodn-table { + display: table; + margin: 1.5em 0px; + vertical-align: baseline; + font-weight: bold; +} + +.prodn-column-group { + display: table-column-group; +} + +.prodn-column { + display: table-column; +} + +.prodn-row-group { + display: table-row-group; +} + +.prodn-row { + display: table-row; +} + +.prodn-cell-nonterminal, +.prodn-cell-op, +.prodn-cell-production +{ + display: table-cell; +} + +.prodn-cell-nonterminal { + padding-right: 0.49em; +} + +.prodn-cell-op { + padding-right: 0.90em; + font-weight: normal; +} + +.prodn-table .notation > .repeat-wrapper { + margin-top: 0.28em; +} + +.prodn-table .notation > .repeat-wrapper-with-sub { + margin-top: 0.28em; + margin-bottom: 0.28em; } /* We can't display nested blocks otherwise */ diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js index 63112312d0..d2eee1f5fa 100644 --- a/doc/sphinx/_static/notations.js +++ b/doc/sphinx/_static/notations.js @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css index 9d133fb1aa..aa4180d246 100644 --- a/doc/sphinx/_static/pre-text.css +++ b/doc/sphinx/_static/pre-text.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ |