/[mojave]
ViewVC logotype

Revision 3057


Jump to revision: Previous Next
Author: jyh
Date: Sun Sep 10 18:26:37 2000 UTC (20 years, 10 months ago)
Changed paths: 121 (showing only 100; show all)
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.


Changed paths

Path Details
Directorymetaprl/doc/latex/ added
Directorymetaprl/doc/latex/theories/ added
Directorymetaprl/doc/latex/theories/Makefile added
Directorymetaprl/doc/latex/theories/README added
Directorymetaprl/doc/latex/theories/all-theories.bbl added
Directorymetaprl/doc/latex/theories/all-theories.tex added
Directorymetaprl/doc/latex/theories/base/ added
Directorymetaprl/doc/latex/theories/base/print.ml added
Directorymetaprl/doc/latex/theories/czf/ added
Directorymetaprl/doc/latex/theories/czf/print.ml added
Directorymetaprl/doc/latex/theories/fol/ added
Directorymetaprl/doc/latex/theories/fol/print.ml added
Directorymetaprl/doc/latex/theories/itt/ added
Directorymetaprl/doc/latex/theories/itt/print.ml added
Directorymetaprl/doc/ps/ added
Directorymetaprl/doc/ps/theories/ added
Directorymetaprl/editor/ml/ modified , props changed
Directorymetaprl/editor/ml/Makefile modified , text changed
Directorymetaprl/editor/ml/shell.ml modified , text changed
Directorymetaprl/editor/ml/shell_package.ml modified , text changed
Directorymetaprl/editor/ml/shell_sig.mlz modified , text changed
Directorymetaprl/editor/ml/shell_state.ml modified , text changed
Directorymetaprl/editor/ml/shell_tex.ml added
Directorymetaprl/editor/ml/shell_tex.mli added
Directorymetaprl/filter/base/Files modified , text changed
Directorymetaprl/filter/base/filter_cache.ml modified , text changed
Directorymetaprl/filter/base/filter_cache_fun.ml modified , text changed
Directorymetaprl/filter/base/filter_comment.ml modified , text changed
Directorymetaprl/filter/base/filter_prog.ml modified , text changed
Directorymetaprl/filter/base/filter_spell.ml added
Directorymetaprl/filter/base/filter_spell.mli added
Directorymetaprl/filter/base/filter_summary.ml modified , text changed
Directorymetaprl/filter/base/filter_summary.mli modified , text changed
Directorymetaprl/filter/base/filter_summary_type.ml modified , text changed
Directorymetaprl/filter/base/filter_type.ml modified , text changed
Directorymetaprl/filter/filter/filter_main.ml modified , text changed
Directorymetaprl/filter/filter/filter_parse.ml modified , text changed
Directorymetaprl/filter/filter/filter_parse.mli modified , text changed
Directorymetaprl/mllib/ modified , props changed
Directorymetaprl/mllib/Makefile modified , text changed
Directorymetaprl/mllib/comment_parse.mli added
Directorymetaprl/mllib/comment_parse.mll added
Directorymetaprl/refiner/reflib/dform.ml modified , text changed
Directorymetaprl/refiner/reflib/rformat.ml modified , text changed
Directorymetaprl/refiner/reflib/rformat.mli modified , text changed
Directorymetaprl/refiner/reflib/simple_print.ml modified , text changed
Directorymetaprl/theories/base/.ispell_english added
Directorymetaprl/theories/base/Makefile modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.ml modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.mli modified , text changed
Directorymetaprl/theories/base/base_dform.ml deleted
Directorymetaprl/theories/base/base_dform.mli deleted
Directorymetaprl/theories/base/base_dtactic.ml modified , text changed
Directorymetaprl/theories/base/base_rewrite.ml modified , text changed
Directorymetaprl/theories/base/base_theory.mlz modified , text changed
Directorymetaprl/theories/base/base_trivial.ml modified , text changed
Directorymetaprl/theories/base/summary.ml deleted
Directorymetaprl/theories/base/summary.mli deleted
Directorymetaprl/theories/base/typeinf.ml modified , text changed
Directorymetaprl/theories/czf/ modified , props changed
Directorymetaprl/theories/czf/Makefile modified , text changed
Directorymetaprl/theories/czf/czf_itt_all.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_all.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_all.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_and.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_and.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_and.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_axioms.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_axioms.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_comment.ml added
Directorymetaprl/theories/czf/czf_itt_comment.mli added
Directorymetaprl/theories/czf/czf_itt_comment.prla added
Directorymetaprl/theories/czf/czf_itt_dall.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dall.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_dall.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_dexists.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dexists.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_dexists.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_empty.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_empty.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_empty.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq_inner.prlb deleted
Directorymetaprl/theories/czf/czf_itt_exists.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_exists.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_exists.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_false.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_fol.mlz added
Directorymetaprl/theories/czf/czf_itt_fol.prla added
Directorymetaprl/theories/czf/czf_itt_implies.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_implies.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_implies.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_infinity.ml deleted
Directorymetaprl/theories/czf/czf_itt_infinity.mli deleted
Directorymetaprl/theories/czf/czf_itt_infinity.prla modified , text changed
Directorymetaprl/theories/czf/czf_itt_isect.ml added
Directorymetaprl/theories/czf/czf_itt_isect.mli modified , text changed
Directorymetaprl/theories/czf/czf_itt_isect.prla added
[...]

  ViewVC Help
Powered by ViewVC 1.1.26