/[mojave]/metaprl/theories/tactic/comment.ml
ViewVC logotype

Log of /metaprl/theories/tactic/comment.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 4538)

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 41817 byte(s)
Diff to previous 3584
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).


Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 1 month ago) by nogin
File length: 41544 byte(s)
Diff to previous 3235
- 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.


Revision 3235 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 41532 byte(s)
Diff to previous 3223
Display form fixes.

- TeX: all object-level terms (theorem statements, etc) are now typeset
in math mode.

- Tex: variable names are now parsed to detect indeces. In particular,
  'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.

- Tex: `|' symbol in display forms is now always handled correctly.

- Numerous small fixes.


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 41815 byte(s)
Diff to previous 3222
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3222 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 22:00:34 2001 UTC (20 years, 1 month ago) by nogin
File length: 41970 byte(s)
Diff to previous 3220
- Fixed slot["raw", ...]
- Fixed couple small typos.


Revision 3220 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 17:57:28 2001 UTC (20 years, 1 month ago) by nogin
File length: 41958 byte(s)
Diff to previous 3212
Reverting the last change I did on dforms in this file - that was a mistake.


Revision 3212 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 6 21:08:07 2001 UTC (20 years, 1 month ago) by nogin
File length: 41958 byte(s)
Diff to previous 3058
A few display form fixes.


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Added Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 41958 byte(s)
Last commit failed partway through...


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26