Annotations

Among the two types of Pages, annotations are best for writing shorter, simpler notes, and they can be used to attach example explorers or other brief commentary to nodes or deductions.

Format

An annotation looks something like this:

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

or this:

anno Notes on Pf.A10 @@@
Here are some comments on node A10 in Pf.
@@@

The general format is:

Listing 63 Annotation format

anno NAME [on TARGET] @@@
    CONTENTS
@@@

where

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

• CONTENTS are written in Markdown, with Widgets.

• The optional on TARGET clause can be used to attach the annotation to a node or deduction. Here, TARGET is a relative libpath resolving to the desired object.

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

Attachments

When the on TARGET clause (see Listing 63) is used to attach an annotation to a node or deduction, then, when users right-click the target node or deduction in PISE, the context menu will list the annotation as an available enrichment.

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 64 Widget format for annotations

<TYPE:NAME>[LABEL]{DATA}

where TYPE, NAME, LABEL, and DATA are The four widget components.

Omissions

When optional components are omitted, the surrounding brackets are still written. Thus, a widget that takes no LABEL has this form:

<TYPE:NAME>[]{DATA}

while a widget defining neither NAME nor LABEL has this form:

<TYPE:>[]{DATA}

The DATA component

Viewed in isolation, the {DATA} part of a widget definition, i.e. the DATA component together with the surrounding braces, looks exactly like the definition of an object in Proofscape-flavored JSON:

<TYPE:NAME>[LABEL]{
    it: "might",
    look: null,
    something: {
        like: 1,
        this: 2,
    }
}

Thus, the field names appear as the keys of the object, and, as usual, you are free to omit quotation marks around these.

You are also free (and encouraged) to use linebreaks and indentation to improve readability, as shown above. See, for example, Listing 11 in the Authors Tutorial.