Sphinx Pages#

As discussed in rst files, one Sphinx page is defined for each rst file in a Proofscape repo. The pfsc directive was also covered there. Most of what remains to be covered here regards the details of widgets in Sphinx pages. We also cover the required files that must be present in a Proofscape repo in order to build Sphinx pages at all.

This reference does not cover rST itself, or Sphinx syntax, since these work exactly the same way in Proofscape as they do in Sphinx. (The Proofscape software uses the Sphinx Python package internally.) Please consult the Sphinx docs on these topics.

Required files#

As illustrated in Part 3: Sphinx Pages of the Tutorial for Authors, any Proofscape repo that wants to define any Sphinx pages must have two required files, both of which are defined in the root directory of the repo: conf.py, and index.rst.

`conf.py`#

Every Sphinx project needs a conf.py. When you build a Proofscape repo that defines any rst files, then the Sphinx build process becomes a step in the overall Proofscape build, and so you must define a conf.py that can be passed to Sphinx.

Among all the Sphinx configuration options, only a few are needed in Proofscape, and not all are supported.

Fields you are encouraged to define are:

html_title: A title to appear on all Sphinx pages
copyright: Copyright information to appear on all pages

Among the configuration options that are not available to you are:

html_theme
extensions

These options are automatically set by Proofscape in a fixed way, in order to generate pages that will work properly when displayed in content panels within PISE, the Proofscape Integrated Study Environment. It’s important to remember that the HTML pages you are building are designed to be viewed there, not on an arbitrary, standalone web site.

Root level `index.rst`#

As in any Sphinx project, the collection of rst files you define in a Proofscape repo (if any) are going to form a hierarchical collection of pages. The hierarchy or tree structure is determined by your use of the Sphinx toctree directive. Usually it mirrors the filesystem tree of directories and rst files you define, and, like any tree, it needs a root. The index.rst file you define at the top level of your Proofscape repo is that root.

To put this another way, the page you build in your root level index.rst is the “start page” to your whole collection of Sphinx pages. Like the opening pages of a book, it can present a title, introductory text, and, critically, a table of contents from which all the other sections and pages can be found. See Defining document structure in the Sphinx docs.

Prohibited filenames#

In order to avoid collisions with certain pages that Sphinx automatically generates, you may not define files with any of the following names, at the root level of your Proofscape repo:

genindex.rst
search.rst

Widgets#

Whereas there is just a single format for widgets in annotations, in Sphinx pages widgets can be written in three different ways, using rST roles, directives, and substitutions.

Roles and Directives#

The rST language provides an extension mechanism whereby custom roles and directives may be defined, and Proofscape takes advantage of this mechanism to give you a way to define Proofscape widgets within Sphinx pages.

Because Proofscape’s custom roles and directives have to exist within the same namespace as all the built-in roles and directives belonging to rST and to Sphinx, their names will always begin with pfsc-, in order to set them apart.

Roughly speaking, a role (more formally, an interpreted text role in rST parlance) is an inline construction, meaning that you can use it without introducing a paragraph break, whereas a directive is a block construction, meaning that to use it does require a paragraph break.

For example, Listing 65 shows valid rST that defines two Proofscape chart widgets, one in role form, and one in directive form.

Listing 65 Example of valid rST defining two chart widgets#

A Proofscape chart widget *in role form* might look :pfsc-chart:`like this <Pf.A10>`,
and can fit into the overall flow of a paragraph. On the other hand, the
*directive form* of a chart widget appears like this:

.. pfsc-chart:: I am a chart widget in directive form
    :view: Pf.A20

and forces a paragraph break.

Not every widget type in Proofscape offers both a role and a directive form, but the chart widget is one that does. (For further details, see Chart Widgets.) In general, when a role form is offered, it is designed to be brief, and offers only a limited subset of the full functionality that’s always available in the directive form.

So what happens when you need the full functionality of the directive form, but do not want to introduce a paragraph break? Read on. We answer this question when we discuss the Substitution format.

`SUBTEXT`#

Before we can define the three widget formats, we need one additional concept, which we call the SUBTEXT. (Note: this has nothing to do with a “subtext” in the sense of an “underlying meaning in a literary work!” It is just a convenient term we have co-opted for use here.)

The SUBTEXT is a place where you can define one, or the other, or both, of the NAME and LABEL for a widget. The legal formats are described in Table 12.

Table 12 Acceptable formats for `SUBTEXT`#
Format	Explanation
`NAME: LABEL`	Defines both the `NAME` and the `LABEL`.
`NAME:`	Defines just the `NAME`.
`LABEL`	Defines just the `LABEL`. The `NAME` will be system-generated. The `LABEL` cannot contain any colons (`:`).
`: LABEL`	Defines just the `LABEL`. The `NAME` will be system-generated. The `LABEL` may contain colons (`:`).

The three widget formats#

Just as in annotations, defining a widget means defining The four widget components of TYPE, NAME, LABEL, and DATA. In Sphinx pages, this can be done using one of three different formats, which we call the role, directive, and substitution formats.

Listing 66 offers a summary of the three formats. In the following sections, they are explained in detail.

Role format#

Listing 67 Role format for widgets in Sphinx pages#

:pfsc-TYPE:`SUBTEXT <ROLE_FIELD>`

Not all widget types support role format. When a given widget type does support role format, it selects a single one of its DATA fields to be its ROLE_FIELD. This is the only field that you can define, if you use role format. If you need to define more fields than this one, then you have to use either the directive or the substitution format instead.

For example, the ROLE_FIELD for chart widgets is view, and that for doc widgets is sel. (See Widget Specs.)

The widget TYPE appears in the role name (e.g. the chart in pfsc-chart), while you can use the SUBTEXT to set the NAME and/or LABEL.

Directive format#

Listing 68 Directive format for widgets in Sphinx pages#

.. pfsc-TYPE:: SUBTEXT
    :field_1: value_1
    :field_2: value_2
    ...
    :field_n: value_n

    CONTENT_FIELD

In directive format (as in role format), the TYPE of the widget appears in the name of the directive, while you can use the SUBTEXT to set the NAME and/or LABEL.

This just leaves the DATA fields. For the most part, these are given as directive options, illustrated as :field_1: value_1, :field_2: value_2, etc. in the listing above. Each :field_i: just puts a field name between colons. The format of each value_i depends on the widget type and the field, but is always given in Proofscape-flavored JSON.

The one exception is the CONTENT_FIELD. Each widget type may or may not assign one of its fields to be a CONTENT_FIELD, meaning that:

You must provide its value as directive content, i.e. in an indented block under the directive, separated by one blank line.
Its value is always interpreted as a string, but you do not surround it with quotation marks of any kind.

Generally speaking, a CONTENT_FIELD will only be assigned to a field whose value tends to be multi-line and potentially quite long.

Substitution format#

Listing 69 Substitution format for widgets in Sphinx pages#

|SUBTEXT|

.. |SUBTEXT| pfsc-TYPE::
    :field_1: value_1
    :field_2: value_2
    ...
    :field_n: value_n

    CONTENT_FIELD

Substitution format provides a way to utilise all the power of the directive format, while allowing the widget to appear inline, i.e. in the midst of a paragraph. Of course, this only makes sense for widget types whose graphical appearance is inline, such as chart and doc widgets.

Here we make use of rST substitutions, which consist of two parts: an inline substitution reference, which can lie in the middle of a paragraph, and a block substitution definition, which comes after the paragraph, or even at the bottom of the page. For the inline reference, you simply write the SUBTEXT surrounded by pipe characters |. In the definition coming after the paragraph, you repeat this, and then define the widget in directive format.

For example, we could use the substitution format to define a chart widget like this:

Let's open the |w1: proof|.

.. |w1: proof| pfsc-chart::
    :view: Pf
    :color:
        bgB: Pf.A03

Here, our SUBTEXT is w1: proof, and it defines the widget’s NAME to be w1, and its LABEL to be proof. When the page is rendered as HTML, only the word “proof” will appear as the clickable text that represents the widget, at the end of the sentence “Let’s open the proof.” The widget name w1 is automatically cut out of the SUBTEXT, and does not appear.

Design rationale#

Why is the SUBTEXT designed to support both NAME and LABEL definitions, as described in Table 12? And why is it called “subtext”? The key idea is that the NAME actually serves two purposes here. One, of course, is to give the widget a name (so that it has a libpath, and can be referenced). The additional purpose is to make the substitution text unique.

For example, consider what would happen if you wanted to use the substitution pattern to define a couple of chart widgets, and you wanted their label text to be the same. Somewhere, perhaps near the beginning of a long page, you might write

Let's take a look at |the proof|.

If the NAME couldn’t be a part of the SUBTEXT, then this would be the last time on this page that you could use “the proof” as the LABEL text of any widget. While it’s sometimes important stylistically to try to vary label text, it would be a problem if phrases could be “used up” in this way.

By including a NAME in each SUBTEXT, all substitutions can be unique (as rST sees them), while the displayed LABEL can still be the same. For example:

Gauss offered several different proofs of this theorem. Here is |Pf1: one|.
Here are |Pf2: another| and |Pf3: another|.

In the rendered page, each of the last two widgets will display the exact same text (“another”), and yet they can represent two distinct chart widgets, which can link to two different proofs.