- fixed logging in log window so that spurious html tags are no longer
  printed
- factorized a lot of error handling code in invokeTactics
- moved (and reimplemented) logger class to ui_logger module

renamed module "logger" to "cicLogger" to avoid confusion with user
interface logger

sample script.sh which read META files from ocaml/METAS

moved META files in METAS/ dir

added support for cic_textual_parser2 module

new experimental cic textual parser: checkin

close RC bug regarding rebuilding with newer gthmathview

mathql documentation for version 4

debian version 0.0.4-3

added -thread option where needed to make new findlib happy

ignore environments

esplicitely add -thread parameter to all compiler invocations

use a list of getter maps

rebuilt

sort CProp added

The tmp is now cleared from the http___* files.

updated

* debugging messages and dumpes commented out

Porting to lablgtk2 completed.

The hbugs client interface is almost working again.

HBugs compile again (but it does not do anything right now: still to be
ported correctly to lablgtk2)

First release that compiles under lablgtk2 (but it does not work, actually!)

updated to version 4

updated to version 1.4

* first upgrade to the new error logging mechanism

*** empty log message ***

some interfaces changed to prepare the mathql code for version 1.4

* removed dependency from liblablgtk-ocaml{,-dev}

* added profiling options

* temporarily removed hbugs dependency

* updated for gtk2
* temporarily removed hbugs
* temporarily removed html widget using a plain text widget instead

* updated for gtk2

debian version 0.0.4-2

* this implements the new instantiation for gtkmathview

* GEdit -> GText

* variant types changed for selection mode

* fixed O_S variable for ocamlmklib on hppa arch

- debian release 0.0.6-3
- use .o objects from .libs directory so that they are PIC
  (fix build failure on hppa)

* first version of the profile manager committed

* added timer for profiling the editor

* added daemon
* fixed minor bugs

* oo interface

* first files added to cvs

debian version 0.5.1-2

debian version 0.5.1-1

debian snapshot version 0.0.6-2

* snapshot for gtk2

* added new .ml files to be ignored

* lablgtk -> lablgtk2

* removed debugging Printfs'

* removed currified constructors everywhere. A bug in the ocaml compiler
  allowed to use them, but the bug is now fixed so they cannot be used
  anymore. Sorry fellows, next time choose a better compiler ;-)

hxp: performes several tasks among which some metadata extraction

* minor fix

* removed spec file
* updated configuration
* added .props file for lablgtk2

* upgrade to lablgtk2

* checking for lablgtk2

* update dependency: lablgtk -> lablgtk2

* added popup menu, implemented some functions

debian package for ocaml 3.07

* changed version in configure.ac
* gdome_xslt.c renamed into x_gdome_xslt.c otherwise there was a conflict
  with make rules that prevented gdome_xslt.o from being built correctly

* further code cleanup

* updated #include directives
* clean up of some makefiles

* the main function MUST return 0 to communicate everything was OK

* new version of metadata extraction
* metadata are inserted directly without creating the RDF document

* the regular expressions must have $ otherwise the shortest match
  will be found first and the annotations will never show up

...

Reindentation.

ProofEngine.goal :=   ==>   set_proof_engine_goal

Reindentation

ProofEngine.proof is now an abstract data type (since we plan to have OMDoc
in the future as the persistent format).

patch

This version of xmlDiff is much much much smarter than the previous one:
with the forthcoming version of gdome the performances will be doubled.
[ Unfortunately, it is still deadly slow. ]

Reindentation

BU_Conversion + omit-conclusion is a mess. I have partially fixed the
problem by ignoring the omit-conclusion flag.

Debugging stuff removed.

Now mathql_generator compiles before mathql_interpreter.
This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator.

Preliminary support for proof-tree enhanced: proof-trees are now shown
as views over .con files.

- added support for proof trees
- fixed typo in body.ann regexp

clean_cache method added

cleancache ==> clean_cache

Clean cache method added.

param.framewidth = 150 (hard-coded ;-(    pour Hanane ;-((((((((((

Following an hyperlink from a proof-tree rendering now brings you to
the lambda-term rendering of the proof statement.

Preliminary commit to support Hanane's proof-tree rendering.

prop.media-type and prop.encoding were _NOT_ considered when the
corresponding HTML <meta/> was generated. Fixed.

www-sop.inria.fr
   ^
Hyphen in the name of the server were not allowed. Fixed.

- bumped copyright years
- added support for proof checker environment dump/save/restore
- added support for hbugs notify upon goal change (disabled by default)
- added (re)submit option to hbugs menu

- converted TAB to spaces

- clear hints list upon status submit
- converted TAB to spaces

- added support for dumping environment to file on exit (disabled by default)
- added environment restore on boot

added environment setting (set by fill_template)

added environment file setting for each tutor

added support for dump/restore/clear proof checker cache

added notation for reals 0, 1, n

* small fixes for distribution

* fixed dependency on gtkmathview 0.5.1

* added licence to IDL file

* some code cleanup
* added LICENCE to all source files

* using the clipboard to communicate the id of the selected subtree

* completed implementation of View interface