This commit was manufactured by cvs2svn to create tag 'submitted'.

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

added UWOBO respawner script

getter's panel check in

added a TODO bug comment

ignore comments and blank line in servers file

moved "is_blank_line" from Http_getter_common to Http_getter_misc

added list_servers, {add,remove}_server methods to usage string

updat changelog with list_servers method addition

added "/list_servers" method (actually used by the getter panel)

- added "/add_server" and "/remove_server" to dynamically adjust servers
  list at runtime

- added functions "add_server" and "remove_server" to dynamically adjust
  servers list at runtime

- added functions "add_line" and "remove_line" to edit line oriented files
- use some Zack helpers intstead of reinventing the wheel

added "replace" method which interfaces Dbm.replace function

link also zack's helpers

rebuilt

added zack's helpers

* new semantics with 2 continuations

* version with single continuation