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

New dependencies.

New: stylesheets are now partially cached (i.e. all the stylesheets which
are applied using an empty list of props are now precompiled only when
added or reloaded). See bug #75.

No more used since a long time.

When the stylesheet from TML to MathML generated a document without a root
an assertion failed. The new implementation creates an empty document
(with only a m:math root element) and prints an error message (using the
logger).

The stylesheet used to generate an empty (and not even well-formed) XML document
when given a document whose root element is tml:tex and whose only child
is a non-visible cursor. The problem is fixed generating a <m:math/> document
(ignoring the visibility status of the cursor).

The reset() method ignored the fact that the widget can be frozen. Fixed.

patch

patch

patch

patch

patch

- New interface for the MathQL interpreter (1.3 version)
- Two toplevels committed in ocaml/mathql_test (new directory)

Improved exception catching.

bugfix: print a better exception than "Not_found" when "baseuri"
parameter for "ls" method is empty or simply unparsable

- removed unclear parameter on_exit
- renamed on_use_hint to use_hint_callback
- added method setUseHintCallback

Use of Hbugs_deity for thread creation and killing.

Support for optional state (empty XML element).

- use an exception to handle empty status nodes
- removed some ancient comments

updated serialization test

no longer used (use HBUGS_MESSAGES.xml directly)

- support None state
- added (de)serialization of Too_late

State_change can now contain a state of None indicating that the proof
is completed

added "restart" target

added ocamlfind trick to trigger rebuild when some library's .cma has
been changed

added support for slaves killing

NuPrlDefinition element handling added

extra_info hack removed

@uri attribute added to tacticinstance. A "Tactic details" hyperlink is
now automatically generated starting from it.

The UNICODEvsSYMBOL machinery is now working again.

nuprl_content_to_html.xsl is not used. Let's definitely remove it.

First commit of the NuPRL stylesheets.

kill instances of uwobo_forever.sh on stop

- added support for UWOBO respawner
- added some newline related pretty printing