mathql_interpreter: natile-galax package removed from Makefie and META
mathql_generator  : MQueryLevels2.ml patched (namespaces removed from sorts)

The type of a LetIn is now a LetIn if and only if the bound variable really
occurs.

The "Save proof" menu item is now activated when a finished proof is reopened.

Reindentation.

Reloading bugged stylesheets no longer makes gTopLevel crash.

Reload stylesheets menu entry added (under the Settings menu)

...

http://....#Prop shortened to Prop due to a bug (feature?) in the DB.

relativeDepth function removed (useful only for cooking)

Metadata tools are now working correctly also over .body files.

The proof-checker should now be working also on .body files.

dropBodySuffix function added

- Object URL link added
- rethorical text changed

Ported to the latest version of libhttp

added tons of #include <cassert> to make latest gcc compiler happy

preliminar 0.0.3-2 debian release

forward ported to use pkg-config

It should have already been moved to ocaml/mathql_generator

Removed (it should have already been in ocaml/tactics)

Porting to the latest version of PXP (1.1.94).

No longer in use.

Branch V7_3_new_exportation merged.

Branch V7_3_new_exportation merged.

- help method added
- branch V7_3_new_exportation merged

styles directory creation now works even if stylesheets and meta_stylesheets
are symbolic links (as in my case)

Author specification added in head comments;
MQueryGenerator.builtin ready to be used

...

Installation instructions.

- script.sh added to the repository: you should change it to reflect your
  own settings
- the Makefile tries now to automatically build the styles directory, made
  only of hyperlinks to the styles in stylesheets and stylesheets/generated.
  Before doing make, you have to check out the stylesheets and meta_stylesheets
  repositories from the mowgli archive.
- added rootcontent.xsl which is the version used by gTopLevel until we find
  a better solution. You should change it to reflect your own settings.

New version 0.0.3:
 - tml-litex.xsl was not installed
 - guiGTK.h did not include gdome.h
 - configure.ac was not correctly ported to pkg-config, since it still
   checked for the existence of the *-config executables for all the
   packages editex depends on. Fixed.

* mquery_interpreter logging and debugging activated
* bug fixed: the universe of the complete search pattern must exclude
  the InBody occurrences

The universe was the one of the complete search, not that of the
searchPatter (restricted to the conclusion).

Reindented

Merge of the V7_3_new_exportation branch.

removed old -config script

#include <cassert> patch

debian version 0.0.4-5

New version 0.0.2:

* Bug fixed:
  - the *PushLexer reset method did not notify the PushParser of the
    buffer reset
  - the reset() method of the ocaml binding did not reset the Lexer.
    Closes #85 and #86
  - Even if the cursor is not visible, its value should be rendered
    in MathML Presentation and it should be printed in TeX. Fixed
    both xml-mmlp.xsl and tml-tex.xsl

* New stuff:
  - the LPushLexer now recognized \/ as a long identifier character.
  - Added a new tml-litex.xsl stylesheet from TML to TeX + long identifiers.
    It should be (but it is not yet) the inverse function of the
    parser

* added pkg-config stuff

fixed autoconf variable @@ vs $()

MathQL 1.3 ready for use

debian version 0.4.3 (maybe, not tested)

* removed *-config script invocations, now using pkg-config

bumped version to 0.4.3

No longer used.

* added template for tml:s
* if the cursor is the empty string it is not produced

- tabs removed
- "\" correctly quoted in strings
- in case of self-loops, the process diverged. Self-loops are now
  ignored during parsing.

findlib introduced

* the non-empty cursor is now generated

* patched wrong commit (perhaps...)

new syntax for "property" enabled:
 now many "isfalse" clauses are accepted

final ispell

Minor modifications to the new session.

...

...

color ==> gray

...

New session (the H-Bugs interactive session).

draft review

New ispell.

Several other small changes here and there.

...

thread handling reviewed

Figure moved to the next page.

Several editor notes resolved.

Everything Ispell-ed.

Other references added.
An old part removed.

A new references.

Many references committed.

Some editor notes closed.

Lots of small changes in the text.

extended syntax for add

- several changes in all the parts that made comparisons with MONET
- added a few sentences in the conclusions section

added web-services' interfaces image

- reviewed latest CSC'comments
- added future works
- added an image

site updated

Several small changes to the parts committed by Zack.

added status.eps

written section 3

First part of the chapter about tutors. The automatic generation part is
still missing.

- (badly) written section 2 (Architecture)
- removed old oldparts in introduction, added some ednotes

added architecture figure

added MONET's Math Obj Manager to conclusions

added multiple invocations of latex

Added all (???) the sections and their labels.

Minor improvements in the introduction.

* fix in optional argument for ocaml binding
* fix in tml->mmlp stylehseet

- Introduction changed.
- Tasks assigned.

ed and draftstamp packages committed and activated

mathql query generator interface patched

first checkin
- introduction
- outline
- auxiliary files

patched

MathQL query generator: new interface

Several changes:

1. the UWOBO_LOG_FILE environment variable semantics changed. It is now
   used in the following way: $UWOBO_LOG_FILE.pid.log
2. when the log file can not be opened, UWOBO used to crash. Instead,
   it now goes on and a nice error message is printed on the stderr
   (but, unfortunately, it is not given back to the user, since the
   error is raised in a new process and it can not be read back from
   the logfile!)

The semantics of the UWOBO_LOG variable has changed: the suffix ".log"
should not be in there any more.

The chmod ug+w in the all rule has been made non-critical.

This commit undoes part of the previous commit, where I mistakenly committed
parts of my laptop settings.

New: two methods have been added to kill UWOBO and to start a new session
     (i.e. a new UWOBO process) listening on a given port)

New: two new methods added

* /newsession to create a new session on a given port (i.e. to fork a new
  UWOBO that starts listening on the new given port)
* /kill to ask an UWOBO to finish the execution

MQueryInterpreter: interface updated