Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-10 11:26:37 -0700 (Sun, 10 Sep 2000)
Revision: 3057
Log message:
This jumbo update is a documentation update. There are no
logical changes. I did two things:
1. First, comments that begin with the sequence "(*!" are
interpreted as structured comments. The contents are parsed
as terms, and the comments will display in the editor window.
The comments may contain arbitrary text, as usual, and they
can also contain explicit terms. The syntax for terms is:
@opname[p1, ..., pn]{t1; ...; tm}
or there is an alternate syntax:
@begin[opname, p1, ..., pn]
arg
@end[opname]
Text sequences count as a single term. So, for instance, the
term @bf{Hello world} display the "Hello world" text in a bold
font.
The "doc" term is used for text that is considered to be
documentation. There is a set of LaTeX-like terms that you can
use to produce good-looking documentation. These are all
documented in the theories/tactic/comment.ml module. The exact
syntax of structured comments is defined in the
mllib/comment_parse.mll file. You can also look at any of the
module in the theories/itt directory if you want to see examples.
You can generate a pritable version of documentation with the
print_theory command in the editor. For example, the command
# print_theory "itt_equal";;
produces a file called output.tex that can be formatted with
your favorite version of latex2e. You can also generate a
manule of all the theories by running "make tex" in the
editor/ml directory. Or you can run "make" in the
doc/latex/theories directory.
The files are hyperlinked, and they contain a table of contents
and an index. The preferred reader is acrobat, and the preferred
formatter is pdflatex.
2. Second, I documented the tactic, base, itt, and czf theories.
3. Oh, and I also added a spelling checker:) You can turn on the
spelling checker with the -debug spell option or MP_DEBUG=spell.
If prlc thinks that your files contain spelling mistakes, it will
print them out and abort. You can fix this problem by 1) fixing
the spelling error, 2) adding the words withing a @spelling{words}
term in a comment, or adding the words to you .ispell_english
directory.
For example, we could either do this:
@begin[spelling]
Aleksey Nogin
@end[spelling]
Or we could just add Alexey to either $cwd/.ispell_english, or
~/.ispell_english.
The spell checker uses /usr/dict/words as a database, which it
compiles to a hashtable in /tmp/metaprl-spell-$USER.dat. Don't
worry about the tmp file, it is generated automatically.