Deftutorial
Generate utilities to build a tutorial.
A tutorial, in the ACL2+Books documentation,
may often consist of a collection of manual pages (i.e. XDOC topics)
organized in a sequence.
The pages are meant to be read, at least the first time, in that order.
It is generally convenient for these pages to include
`next' and `previous' links to navigate through the sequence.
The deftutorial macro generates macros that can be used to
build a tutorial with the structure described above,
in which the `next' and `previous' links are generated automatically
based on the order in which the tutorial pages are defined in the file.
The way deftutorial works is perhaps most easily explained
through a simple (artificial) example.
The user starts with a (top-level) call
to generate the macros used for defining the tutorial pages:
(deftutorial my-tutorial "My tutorial")
Here, my-tutorial is a symbol that names the tutorial.
This could be any symbol, which is used in the names of
the generated macros (and associated functions) described below,
the ACL2 table mentioned below,
and the XDOC topics generated by those macros.
The second argument, "My Tutorial",
is a short description of the tutorial,
used to construct the XDOC short strings of the tutorial pages (see below).
It must be a string that does not end with a period,
because in the generated XDOC short strings
it is followed by a period or colon.
The above call of deftutorial generates the following macros:
- def-my-tutorial-top
- def-my-tutorial-page
- def-my-tutorial-topics
- my-tutorial-section
Note that part of their names is the symbol my-tutorial
passed to deftutorial.
These generated macros are used as follows.
Now the user should make a (top-level) call
to define the top page of the tutorial:
(def-my-tutorial-top
(my-tool my-tutorials)
(xdoc::p
"Here we provide a tutorial for this very good tool.")
(xdoc::p
"Although we are using XDOC constructors here,
we could be using a plain XDOC long string here."))The first argument defines the XDOC parent list.
The remaining arguments must be XDOC constructor trees,
or strings as a special case of trees.
This does not define an XDOC topic yet;
it just stores information about the XDOC topic into a table.
The topic will be called my-tutorial
(so the name passed to deftutorial must be chosen
not to conflict with existing XDOC topics in the manual),
and the table is called my-tutorial-table.
This is the top page of the tutorial,
so it should describe the tutorial in general;
it may also mention that the pages (subtopics)
are organized sequentialy, with bidirectional links.
The parents of this topic is determined by the first argument.
The short string is automatically generated as "My tutorial.",
i.e. the second argument of deftutorial followed by a period.
The long string is obtained by concatenating
the remaining arguments of def-my-tutorial-top.
Then the user should make one or more (top-level) calls
to define the (non-top) pages of the tutorial:
(def-my-tutorial-page first-topic
"The first topic of my tutorial"
(xdoc::p
"Here we discuss the first topic of my tutorial.")
(xdoc::p
"This must consist of zero or more XDOC constructor trees,
or simply XDOC strings (which are also trees)."))
(def-my-tutorial-page second-topic
"The second topic of my tutorial"
(xdoc::p
"Here we discuss the second topic of my tutorial.")
(xdoc::p
"Again, this must consist of zero or more XDOC constructor trees,
or simply XDOC strings (which are also trees)."))
... ; additional pagesSimilarly to the top level page, these do not define XDOC topics yet;
they store their information in the table my-tutorial-table.
Each such call defines a page of the tutorial.
The XDOC topics will be
my-tutorial-first-topic,
my-tutorial-second-topic,
etc.;
i.e. symbol supplied to each all is appended after my-tutorial-
(note the final separating dash).
No explicit XDOC parents are supplied,
because each page has the top tutorial page my-tutorial as only parent.
The XDOC short string is generated by concatenating
the second argument of def-my-tutorial-page
to the second argument of deftutorial with a separating colon,
and a period at the end:
"My tutorial: The first topic of my tutorial.",
"My tutorial: The second topic of my tutorial.",
etc.
The XDOC long string is obtained by concatenating
the remaining arguments of the macro.
The pages must be defined in the sequential order
in which they must be bidirectionally linked in the manual.
Finally, the user should make a (top-level) call
to actually create all the XDOC topics defined above,
augmenting them with links:
(def-my-tutorial-topics)
This reads the information about all the pages from my-tutorial-table
and generates defxdoc calls whose long strings
are augmented by link information at their ends:
- The top tutorial page my-tutorial has
a `start' link to the first page, my-tutorial-first-topic.
- Each non-top page except the last one has
a `next' link to the following page,
e.g. my-tutorial-first-topic has
a link to my-tutorial-second-topic.
- Each non-top page except the first one has
a `previous' link to the preceding page,
e.g. my-tutorial-second-topic has
a link to my-tutorial-first-topic.
The generated macro my-tutorial-section can be called
as part of an XDOC constructor tree to create a section
in a tutorial page (normally the non-top pages).
This may be useful to provide some structure to a long tutorial page,
by providing some ``division'' in the page.
For example:
...
(xdoc::p
"There are three different kinds of this thing.
These are described in the rest of this page.")
(my-tutorial-section "The First Kind")
(xdoc::p
"We describe the first kind here.")
(my-tutorial-section "The Second Kind")
(xdoc::p
"We describe the second kind here.")
(my-tutorial-section "The Third Kind")
(xdoc::p
"We describe the third kind here.")
...
Using this is more abstract than using a specific heading level.
We may extend deftutorial to generate additional macros
like my-tutorial-subsection and my-tutorial-subsubsection
at some point.
Here we use the term `tutorial' in a broad sense.
As should be clear from the above description,
deftutorial is useful to build any kind of
sequentially organized and bidirectionally linked manual pages.
We could rename this macro to something more general at some point,
if some idea for a good general name is proposed.
Subtopics
- Deftutorial-implementation
- Implementation of deftutorial.
