==================== The basic methodology ====================

First, load /slocal/src/acl2/v1-8/emacs/acldoc.elc (making sure that the .elc
file is up-to-date).  The two emacs functions defined there are:

meta-x acldoc-update-marked
  Fix markup of all references to documented topics presently in ~c[].

meta-x acldoc-update-unmarked
  Search for documented topic words in docstrings and query for markup.

It seems ok to abort in the middle of executing either of these functions; on
the next start, you'll simply begin in the current doc topic.

For each file, do meta-x acldoc-update-marked and then acldoc-update-unmarked.
(Or, do the former for all files, then the latter.)  The *acl2-files* are
currently as follows.

("axioms" "basis"
 "translate" "type-set-a" "type-set-b"
 "rewrite" "simplify" "other-processes"
 "induct" "prove" "history-management"
 "defuns" "proof-checker-pkg"
 "proof-checker-a" "defthm"
 "other-events" "ld" "proof-checker-b"
 "tutorial" "interface-raw" "defpkgs")

Note:  I didn't do much with proof-checker-b.lisp, because of the odd nature of
proof-checker documentation.

WARNING:  When the "undo" mechanism of emacs is invoked after an invocation of
either of these two interactive commands, it seems that all work done during
that invocation is undone.  So if you make a single mistake, it's probably best
(after the control-g abort) to manually fix the problem rather than to use
meta-x undo.

Do not link words appearing in the :cite or :cited-by sections of doc strings.
Perhaps acldoc.el should be modified to take away that option.

==================== Additional passes? ====================

It's not clear yet how to handle links for the following concepts, which occur
in the text so much that:

* It's time-consuming to deal with them.
* It's possible that readers will get annoyed with excessive references.

The topics are:  "term", "name", "u".

Until we have more experience, let's postpone these topics.  When we are ready
to deal with them, we should simply load acldoc.el, and then evaluate the
following forms in emacs (e.g., in *scratch* using linefeed, or for each, with
control-x control-e when the cursor is at the end of each).

(setq acldoc-topics
  '("term" "name" "u"))

(setq acldoc-suspect-topics
  '("name" "term" "u"))

(setq acldoc-topics-common-words
  nil)

As suggested below, be careful to omit links for inappropriate uses of words.

a. :DOC name only talks about logical names, so we should link the word "name"
if and only if it is being used in this sense.  However, :DOC name refers both
to event names and variable and constant names.

b. :DOC term talks even about about untranslated terms, so we should almost
always link our use of the word "term".

Also consider rerunning acldoc-update-unmarked on the topics listed in
acldoc-topics-common-words (see acldoc.el).  It should suffice simply to add
any of those of interest into the (setq acldoc-topics ...) form above, and keep
them out of the other two lists.  In particular, consider the following.

"definition", which really does apply to :definition runes but is such a common
word that I don't care to deal with every occurrence of it on the first pass.

"rewrite", which probably occurs a lot.  I prefer to skip all occurrence that
aren't in ~c, because I think that if we were really referring to a rule class
or a rule, we would have written :rewrite and hence have marked it with ~c.

"complex", which is an interesting concept, but whose documentation is really
about the function, not the concept.

"exists".  If we want this linked, we should do so manually, rather than
getting stopped throughout our marking process.  Perhaps we'll notice "forall",
which is not on the list, and that will change our minds.

"logic" and "program", which are defun modes, but should be written as :logic
and :program when they are meant that way, in which case they should be marked
with ~c.

"theory", which is really just the name of a function.  The pointer here is
really to "theories", but I don't want to mess with that right now.

==================== Checking for gross errors ====================

To check that code wasn't changed, start up nacl2 and:

(include-book "/slocal/src/acl2/v1-8/emacs/compare-files")

:q

(LP!)

(compare-files "defthm.lisp" "defthm-orig.lisp" state)

-- the result should be (value nil).

or,

(compare-acl2-files dir1 dir2)
e.g.,
(compare-acl2-files "./" "saved-march4/")

==================== When to link ====================

The big question is:  When should we create invisible links?  Here are some
guidelines.

1. Try not to duplicate explicit links (~l, ~pl) with invisible links (~ilc,
~il), but don't try too hard.  In a very few cases, we might extend this
idea to avoid linking a word anywhere in a doc topic.  For example, I don't
have any invisible links on "guard" in :doc guard-quick-reference.

2. Be sure to link only when the word is being used in the technical sense, or
very very close to it (so that a pointer is clearly in order).  For example, in
order to receive a link, "definition" should refer to a kind of rune, and
"equal" should refer quite directly to the ACL2 function EQUAL.  In fact, those
two examples are removed via the emacs variable acldoc-topics-common-words from
consideration.  A more interesting example is "command", which is linked only
when there is world-changing involved.  (Maybe that's getting carried away...)
There are more reasonable examples, too:  for example, "enable" is not linked
in the context of break-rewrite, and "breaks" is hardly ever linked because
that topic has to do with breaks into raw Lisp.

3. Follow the following dictum:  None of this is all that important, so do
what's easy.  Note that an easy approach is to mark when in doubt -- we can
always go back and look for ~ilc[term] etc., and remove marks.

4. Do not link "documentation" when there's a danger that someone will click on
that to get to a particular documentation topic.  Here is an example.

....
  where each ~il[signature] is as described in the documentation for
  ~il[signature], each ~il[signature] describes a different function
  symbol, and each ~c[evi] is an embedded event form as described in the
  documentation for ~il[embedded-event-form].  There must be at least
  one ~c[evi].  The ~c[evi] inside ~ilc[local] special forms are called ``local''
  ~il[events] below.  Events that are not ~ilc[local] are sometimes said to be
  ``exported'' by the encapsulation.

5. When in doubt, link.