/[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 3584 - (hide annotations) (download)
Thu Apr 25 15:28:40 2002 UTC (19 years, 3 months ago) by nogin
File size: 1323 byte(s)
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.

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 nogin 3584 print_theory "comment";;
38 jyh 3057
39     (*
40     * -*-
41     * Local Variables:
42     * Caml-master: "compile"
43     * End:
44     * -*-
45     *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26