deftutorial-doc

(in-package "ACL2")

(defxdoc deftutorial
  :parents (std/util)
  :short "Generate utilities to build a tutorial."
  :long (topstring (p "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.")
    (p "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.")
    (p "The user starts with a (top-level) call
     to generate the macros used for defining the tutorial pages:")
    (codeblock "(deftutorial my-tutorial "My tutorial")")
    (p "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.")
    (p "The above call of @('deftutorial') generates the following macros:")
    (ul (li "@('def-my-tutorial-top')")
      (li "@('def-my-tutorial-page')")
      (li "@('def-my-tutorial-topics')")
      (li "@('my-tutorial-section')"))
    (p "Note that part of their names is the symbol @('my-tutorial')
     passed to @('deftutorial').
     These generated macros are used as follows.")
    (p "Now the user should make a (top-level) call
     to define the top page of the tutorial:")
    (codeblock "(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."))")
    (p "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').")
    (p "Then the user should make one or more (top-level) calls
     to define the (non-top) pages of the tutorial:")
    (codeblock "(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 pages")
    (p "Similarly 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.")
    (p "Finally, the user should make a (top-level) call
     to actually create all the XDOC topics defined above,
     augmenting them with links:")
    (codeblock "(def-my-tutorial-topics)")
    (p "This reads the information about all the pages from @('my-tutorial-table')
     and generates @(tsee defxdoc) calls whose long strings
     are augmented by link information at their ends:")
    (ul (li "The top tutorial page @('my-tutorial') has
      a `start' link to the first page, @('my-tutorial-first-topic').")
      (li "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').")
      (li "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')."))
    (p "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:")
    (codeblock "..."
      ""
      "(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.")"
      ""
      "...")
    (p "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.")
    (p "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.")))