/[mojave]/metaprl/doc/latex/theories/base/print.ml
ViewVC logotype

Annotation of /metaprl/doc/latex/theories/base/print.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3057 - (hide annotations) (download)
Sun Sep 10 18:26:37 2000 UTC (20 years, 10 months ago) by jyh
File size: 1298 byte(s)
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.

1 jyh 3057 (*
2     *
3     * ----------------------------------------------------------------
4     *
5     * Copyright (C) 2000 Jason Hickey, Caltech
6     *
7     * This program is free software; you can redistribute it and/or
8     * modify it under the terms of the GNU General Public License
9     * as published by the Free Software Foundation; either version 2
10     * of the License, or (at your option) any later version.
11     *
12     * This program is distributed in the hope that it will be useful,
13     * but WITHOUT ANY WARRANTY; without even the implied warranty of
14     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15     * GNU General Public License for more details.
16     *
17     * You should have received a copy of the GNU General Public License
18     * along with this program; if not, write to the Free Software
19     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
20     *
21     * Author: Jason Hickey
22     * jyh@cs.caltech.edu
23     *)
24    
25     set_tex_file "../../doc/latex/theories/base/theory.tex";;
26    
27     print_theory "base_theory";;
28     print_theory "summary";;
29     print_theory "mptop";;
30     print_theory "var";;
31     print_theory "top_tacticals";;
32     print_theory "top_conversionals";;
33     print_theory "base_trivial";;
34     print_theory "base_auto_tactic";;
35     print_theory "base_dtactic";;
36     print_theory "base_rewrite";;
37    
38     (*
39     * -*-
40     * Local Variables:
41     * Caml-master: "compile"
42     * End:
43     * -*-
44     *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26