PRINT-HTML : UTILITYPRINT-HTML is an utility.
PRINT-HTML outputs help messages in HTML format, with links to the
other help messages in TPS. It takes three arguments:
PRINT-HTML "arbitrary string" "/home/theorem/tps/doc/htmldoc/" ignore-tags
where the first argument is any string and the second argument is a prefix
which should be a string containing the URL of the home directory of the
TPS documentation. The third argument is optional, defaulting to NIL;
if it's set to T, then PRINT-HTML will attempt to preserve existing HTML tags
in the input string while still producing correct HTML output; if NIL, it won't
try to do this. Output is produced on the screen, using the MSG command; it's
up to the user to redirect it to a file (see the help messages for
REROUTE-OUTPUT and REROUTE-OUTPUT-APPEND) or a string (using the lisp
function (with-output-to-string (*standard-output*) <form>)).
PRINT-HTML "The flag NUM-OF-DUPS" "/users/foo"
The flag <a href="/users/foo/num-of-dups.html">NUM-OF-DUPS</a>
The URL prefix should usually be the localised version given
above, but if you're running this on a system outside CMU and you want to
link to the documentation at CMU, use the prefix
TPS documentation homepage