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:
anno NAME @@@
CONTENTS
@@@
where
Locations and libpaths#
Annotations can be defined in two places:
At the top level of a
.pfsc
fileInside 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:
<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
, thenA.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.