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 in this section of the reference manual 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.

This reference does not cover rST 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#

When it comes to documenting widgets in Sphinx pages in Proofscape, we take the approach that you should be familiar with widgets in annotations first. Since the widgets that you can build into Sphinx pages are designed to do exactly the same things they do when they appear in annotation pages, our only job here is to tell you how the syntax differs. We won’t repeat everything about what the widgets do, because that would be redundant.

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 42 shows valid rST that defines two Proofscape chart widgets, one in role form, and one in directive form.

Listing 42 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.

The three widget formats#

When we covered widgets in annotations, we explained that each widget is defined by four basic components:

a TYPE,
an optional NAME,
an optional LABEL, and
a collection of DATA fields.

This is true for widgets wherever they are defined – in annotations, or in Sphinx pages. What differs is the syntax you use to define the four components.

Whereas in annotations there is just a single widget format, for Sphinx pages there are three formats, which we call the role, directive, and substitution formats.

Before we can define these 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 (`:`).

With the concept of the SUBTEXT in hand, we can now describe the three different widget formats for Sphinx pages. Listing 43 offers a summary of the three forms. In the following sections, we explain the different formats in detail.

Role format#

Listing 44 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 the various Widget specs by type.)

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

Directive format#

Listing 45 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, illsutrated as :field_1: value_1, :field_2: value_2, etc. in the listing above. Each :field_i: is just a field name; the format of each value_i depends on the widget type and the field.

In addition, 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. Generally speaking, a CONTENT_FIELD will only be assigned to a field whose value tends to be multi-line and quite long.

Substitution format#

Listing 46 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. In the inline reference, you simply set the SUBTEXT (surrounded by pipe characters |). In the definition coming after the paragraph, you 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 |w001: proof|.

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

Here, our SUBTEXT is w001: proof, and it defines the widget’s NAME to be w001, 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 w001 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, especially on widgets that are close together on the page, 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.