Tweaked new function (save-rendered).

acl2 · Sep 22, 2016 · 80898ff · 80898ff
1 parent 286596d
commit 80898ff
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 4 deletions.
diff --git a/books/doc/top.lisp b/books/doc/top.lisp
@@ -462,10 +462,7 @@
 ; but WITHOUT ANY WARRANTY; without even the implied warranty of
 ; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 ; LICENSE for more details.
-
-(in-package \"ACL2\")
-
-(defconst *acl2+books-documentation* '")
+")
 
 (make-event
  (time$
@@ -474,6 +471,7 @@
                     "../system/doc/rendered-doc-combined.lsp"
                     state)
    *rendered-doc-combined-header*
+   '*acl2+books-documentation*
    t ; force-missing-parents-p
    t ; maybe-add-top-topic-p
    state)))

diff --git a/books/xdoc/save-rendered.lisp b/books/xdoc/save-rendered.lisp
@@ -46,10 +46,16 @@
 
 (defun save-rendered (outfile
                       header
+                      topic-list-name
                       force-missing-parents-p
                       maybe-add-top-topic-p
                       state)
 
+; See books/doc/top.lisp for an example call of xdoc::save-rendered.  In
+; particular, the constant *rendered-doc-combined-header* defined in that file
+; is an example of header, which goes at the top of the generated file; and
+; topic-list-name is a symbol, such as acl2::*acl2+books-documentation*.
+
 ; This code was originally invoked with force-missing-parents-p and
 ; maybe-add-top-topic-p both true.  Perhaps that's always best.
 
@@ -82,6 +88,9 @@
          (cw "can't open ~s0 for output." outfile)
          (acl2::silent-error state))
         (state (princ$ header channel state))
+        (state (fms! "(in-package \"ACL2\")~|~% (defconst ~x0 '~|"
+                     (list (cons #\0 topic-list-name))
+                     channel state nil))
         (state (time$ (fms! "~x0"
                             (list (cons #\0 rendered))
                             channel state nil)))