Widgets#

Widgets are interactive elements appearing in Pages.

Current widget types can do things like:

Open, navigate (pan and zoom), and highlight proof charts, so that you can write an animated discussion of a proof. (See examples in the Tutorial for Users.)
Open, navigate, and highlight documents.
Generate interactive and editable mathematical examples using a computer algebra system, so that you can further illustrate the mathematics happening at any given step in a proof.
Present questions, with hidden answers.
Provide checkboxes for users to record their progress.

New widget types may be introduced as time goes on.

The four widget components#

The specific syntax you use to define a widget depends on which type of page you are writing. See:

In all cases, however, there are four components that define a widget:

TYPE is a fixed string indicating the type of the widget. (For the possible values, see the documentation for the various widget types.)
NAME is an optional name for the widget.
- Some widget types require a name; most do not. If you do not provide one, then one will be generated automatically when you build.
- If given, the name must be a string of alphanumerics and underscores, beginning with a letter.
- If the widget is defined in a page of libpath P, then P.NAME is the libpath of the widget.
LABEL is a place where some widget types expect you to provide text. Generally speaking, this is for those widget types that appear as clickable text in the built page.
DATA is a place to define fields to control the behavior of the widget. Fields are given as a set of key-value pairs. The way the keys, or field names, are written depends on whether you are in an annotation or a Sphinx page. Field values are written in a variant of JSON syntax called Proofscape-flavored JSON.

Widget Specs#

In the pages linked below, we provide the precise specification for each of the widget types.

“Format” and “Fields”#

In the spec for each widget type, you will find two sections, headed “Format” and “Fields”, in which we define the rules for The four widget components.

Format#

In the “Format” section we define the following things:

TYPE: The type of the widget.
NAME: Whether a name is required or not.
LABEL: Whether a label is required or not, and, if required, what it does.
ROLE_FIELD: Which of the DATA fields is the ROLE_FIELD, if the Sphinx Role format is supported.
CONTENT_FIELD: Which, if any, of the DATA fields is the CONTENT_FIELD in the Sphinx Directive format.

Fields#

In the “Fields” section we define the required and optional DATA fields accepted by the widget.

For each field, we say which type, or types, are accepted.
We will speak in terms of the basic JSON data types of number, string, boolean, array, object, and null, as well as the additional libpath data type that can be used in Proofscape-flavored JSON. Among numbers, we will sometimes distinguish between int (integer) and float.
When a field accepts any of a finite set of allowed strings as value, we describe its type as enum, and we list the legal strings and their meanings.
When a single field can accept multiple different formats, we describe each format on its own row, and give each row a number for easy reference. These are alternatives, and you should select exactly one (if using the field at all).
When a field calls for a libpath, this always means a relative libpath.