• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Terminal
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
          • Primitive-constructors
            • Generate-primitive-constructor-for-tag
            • Generate-primitive-constructor-for-dir/&&
            • Ul
            • Tt
            • P
            • Code
            • Blockquote
            • Table_
            • Li
            • Color
            • A
            • U_
            • Tr
            • Th
            • Td
            • Sf
            • See_
            • Ol
            • Img
            • I
            • H5
            • H4
            • H3
            • H2
            • H1
            • Dt
            • Dl
            • Dd
            • Br
            • Box
            • B
            • @def
            • &&
            • @{}
            • @url
            • @tsee
            • @sym
            • @srclink
            • @see?
            • @see
            • @measure
            • @gdef
            • @formals
            • @csym
            • @csee
            • @call
            • @body
            • @[]
            • @''
            • @$$
            • @``
          • Composite-constructors
          • Constructor-preliminaries
          • Trees
        • Entities
        • Defxdoc+
        • Save-rendered
        • Add-resource-directory
        • Testing
        • Order-subtopics
        • Save-rendered-event
        • Archive-matching-topics
        • Archive-xdoc
        • Xdoc-extend
        • Set-default-parents
        • Missing-parents
        • Defpointer
        • Defxdoc-raw
        • Xdoc-tests
        • Xdoc-prepend
        • Defsection-progn
        • Gen-xdoc-for-file
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
      • Pointers
      • Doc
      • Documentation-copyright
      • Course-materials
      • Args
      • ACL2-doc-summary
      • Finding-documentation
      • Broken-link
      • Doc-terminal-test-2
      • Doc-terminal-test-1
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Constructors

Primitive-constructors

Primitive XDOC constructors.

These correspond to individual XML tags, individual preprocessor directives, and tree concatenation. In contrast, the composite XDOC constructors correspond to multiple tags, directives, and concatenations, or provide a more concise notation for common attributes.

These primitive constructors are macros with a variable number of arguments. Each argument must be a tree or a keyword, such that each keyword is immediately followed by a tree. Each keyword-tree pair forms an attribute of an XML tag, with the keyword naming the attribute and the immediately following tree providing the value of the attribute. Keyword-tree pairs can be used only in constructors for XML tags, not in constructors for preprocessor directives or tree concatenation. Keyword-tree pairs may occur anywhere in the argument list. See the top-level topic for example calls of primitive constructors.

Since these primitive constructors have a very uniform structure, we introduce them via two event-generating macros, one for XML tags and one for preprocessor directives and tree concatenation.

Subtopics

Generate-primitive-constructor-for-tag
Generate a primitive constructor for an XML tag.
Generate-primitive-constructor-for-dir/&&
Generate a primitive constructor for a preprocessor directive or tree concatenation.
Ul
Construct an XDOC tree for an HTML unordered (bulleted) list <ul>...</ul>.
Tt
Construct an XDOC tree for XDOC inline code <tt>...</tt> (which is not rendered using the homonymous HTML tags; see markup).
P
Construct an XDOC tree for an HTML paragraph <p>...</p>.
Code
Construct an XDOC tree for XDOC code block <code>...</code> (which is not rendered using the homonymous HTML tags; see markup).
Blockquote
Construct an XDOC tree for an HTML quoted block <blockquote>...</blockquote>.
Table_
Construct an XDOC tree for an HTML table <table>...</table>.
Li
Construct an XDOC tree for an HTML list item <li>...</li>.
Color
Construct an XDOC tree for HTML colored text <color>...</color>.
A
Construct an XDOC tree for an HTML hyperlink <a>...</a>.
U_
Construct an XDOC tree for HTML underlined text <u>...</u>.
Tr
Construct an XDOC tree for an HTML table row <tr>...</tr>.
Th
Construct an XDOC tree for an HTML table header cell <th>...</th>.
Td
Construct an XDOC tree for an HTML table cell <td>...</td>.
Sf
Construct an XDOC tree for HTML sans-serif text <sf>...</sf>.
See_
Construct an XDOC tree for an XDOC hyperlink <see>...</see>.
Ol
Construct an XDOC tree for an HTML ordered (numbered) list <ol>...</ol>.
Img
Construct an XDOC tree for an HTML image <img>...</img>.
I
Construct an XDOC tree for HTML italic text <i>...</i>.
H5
Construct an XDOC tree for an HTML level-5 heading <h5>...</h5>.
H4
Construct an XDOC tree for an HTML level-4 heading <h4>...</h4>.
H3
Construct an XDOC tree for an HTML level-3 heading <h3>...</h3>.
H2
Construct an XDOC tree for an HTML level-2 heading <h2>...</h2>.
H1
Construct an XDOC tree for an HTML level-1 heading <h1>...</h1>.
Dt
Construct an XDOC tree for an HTML term <dt>...</dt>.
Dl
Construct an XDOC tree for an HTML description list <dl>...</dl>.
Dd
Construct an XDOC tree for an HTML description <dd>...</dd>.
Br
Construct an XDOC tree for an HTML line break <br>...</br>.
Box
Construct an XDOC tree for an XDOC box <box>...</box>.
B
Construct an XDOC tree for HTML bold text <b>...</b>.
@def
Construct an XDOC tree for a definition directive @(def ...).
&&
Construct an XDOC tree for a concatenation.
@{}
Construct an XDOC tree for a code block directive @({...}).
@url
Construct an XDOC tree for a mangled topic link directive @(url ...).
@tsee
Construct an XDOC tree for a typewriter topic link directive @(tsee ...).
@sym
Construct an XDOC tree for a printed topic link directive @(sym ...).
@srclink
Construct an XDOC tree for a source link directive @(srclink ...).
@see?
Construct an XDOC tree for a conditional topic link directive @(see? ...).
@see
Construct an XDOC tree for a topic link directive @(see ...).
@measure
Construct an XDOC tree for a measure directive @(measure ...).
@gdef
Construct an XDOC tree for a generated definition directive @(gdef ...).
@formals
Construct an XDOC tree for a formals directive @(formals ...).
@csym
Construct an XDOC tree for a capitalized printed topic link directive @(csym ...).
@csee
Construct an XDOC tree for a capitalized topic link directive @(csee ...).
@call
Construct an XDOC tree for a call directive @(call ...).
@body
Construct an XDOC tree for a body directive @(body ...).
@[]
Construct an XDOC tree for a long KaTeK directive @([...]).
@''
Construct an XDOC tree for a inline code directive @('...').
@$$
Construct an XDOC tree for a short KaTeK directive @($...$).
@``
Construct an XDOC tree for an evaluation directive @(`...`).