Annotations#

A Proofscape annotation is essentially just a page of text with interactive widgets that can do a number of things. Current widget types can:

  • Open, navigate (pan and zoom), and highlight proof charts, so that you can write an animated discussion of a proof. (See an example in the Tutorial for Users.)

  • 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.

Annotation pages and proof charts can be displayed side by side in PISE, or even in different browser windows, on two different monitors. This way users can make full use of available screen space, to click through a discussion in one place, and thereby navigate a diagram somewhere else.

As an alternative to annotations, you can also author Sphinx Pages. Sphinx pages are a great way to develop larger works, with tables of contents and all the other features you get with Sphinx. Annotations are still useful as a way to write shorter or simpler notes.

Format#

An annotation looks something like this:

anno Notes @@@
Here are some great notes.
@@@

The general format is:

Listing 40 Annotation format#
anno NAME @@@
    CONTENTS
@@@

where

  • NAME is a string of alphanumerics and underscores, and must begin with a letter.

  • CONTENTS are written in Markdown, plus Widgets.

Locations and libpaths#

Annotations can be defined in two places:

  • At the top level of a .pfsc file

  • Inside a pfsc directive in an .rst file

When defined in a file representing a module of libpath M, an annotation of name NAME has libpath M.NAME.

For example, if an annotation called Guide is defined in a module of libpath host.owner.repo.Ch1.Sec1, then host.owner.repo.Ch1.Sec1.Guide is the libpath of the deduction.

Widgets#

As stated above, the contents of an annotation are basically written in Markdown; however, you are also free to write widgets in the midst of “ordinary text” (i.e. not within headings, boldface, or other special Markdown contexts).

The general format of a widget is:

Listing 41 Widget format for annotations#
<TYPE:NAME>[LABEL]{DATA}

where

  • 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.

    • You do not have to provide a name. 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 an annotation of libpath A, then A.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. The label can simply be left blank in those widget types that do not accept a label (but the [] must still be written).

  • DATA is a place to define key-value pairs, in a variant of JSON syntax called Proofscape-flavored JSON. This is where you define parameters to control the behavior of the widget.

Within the DATA part of a widget definition, you are free (and encouraged) to use linebreaks and indentation to improve readability. See, for example, Listing 11 in the Authors Tutorial.

Widget Types#

In the pages linked below, we provide the precise details for coding each of the widget types. 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 we define the key-value pairs that may be written in the DATA part of a widget, we refer to the keys as fields.

“Format” and “Fields”#

In the specs for each widget type, you will find a section headed “Format,” where we give the rules for the TYPE and LABEL parts of basic widget format defined in Listing 41, and a section headed “Fields,” where we define the rules for all the fields that the widget type accepts in its DATA part.

Specs by type#