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.
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:
Every Sphinx project needs a
conf.py. When you build a Proofscape repo that defines
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:
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.
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.
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.
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:
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.
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
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 collection of
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.)
SUBTEXT is a place where you can define one, or the other, or both, of the
LABEL for a widget. The legal formats are described in Table 12.
Defines both the
Defines just the
Defines just the
Defines just the
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.
.. pfsc-TYPE:: SUBTEXT
.. |SUBTEXT| pfsc-TYPE::
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
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
(See the various Widget specs by type.)
TYPE appears in the role name (e.g.
pfsc-chart), while you can use the
.. pfsc-TYPE:: SUBTEXT
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
This just leaves the
DATA fields. For the most part, these are given as directive options, illsutrated
: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
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.
.. |SUBTEXT| pfsc-TYPE::
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::
w001: proof, and it defines the widget’s
NAME to be
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.
Why is the
SUBTEXT designed to support both
LABEL definitions, as
described in Table 12?
And why is it called “subtext”? The key idea is that the
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|.
NAME couldn’t be a part of the
this would be the last time on this page that you could use “the proof” as the
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.