* 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

* prototypes for auxiliary C++ functions

* advanced implementation of View interface

snapshot

* snapshot

* exceptionset -> exception_set

* update

* code cleanup
* added partial implementation for view

* IDL file update (and renamed)

select and click signal added

added information on the "qdl" article with C.S.C.

use an integer debugging level instead of a boolean one

- use hbugs' describe_callback to render apply-hints on selection
- sync default uri proposed while loading a new proof and loading one
- resend status to hbugs on tab change

commented out gtkmathview's font_size override

added "start" and "stop" targets for hbugs

added support for external configuration of describe_hint_callback

added "describe_hint_callback" invoked when a hint is selected

- removed useless status bar
- hid menu bar
- added (Re)Register button
- added vertical pane between subscription and hints
- changed default size to a "decent"-one

send SIGKILL to stop web services

commented out thread killing (we have to wait for a decent Thread.exit
implementation)

get_childNodes no longer used ==> major performance speed-up

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

added \neqt macro

added notation for Ropp and Rinv

string ==> id

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

fixed associativity of some (all!) binary operators

Replace is now working also over Type.

Replace tactic fixed. It was not working any longer. (It produced a dummy
eta-expansion).

Notation for Rdiv and Rminus.

Debugging infos removed.

string => id

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

replaced with my generic latex makefile

* update with some candidate methods

* added test View interface. It is basically empty but eventually it will host
  any gtkmathview-specific method

- added a destroy callback
- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_

start tutors with nice at the lowest priority

avoid deletion of useful .cmi with .PRECIOUS

commented out debugging tutor "wait"

- added dot notation for real numbers and basic operations on them
- added support for \eqt

- added default URI for new theorems
- added menu items to the hbugs menu for:
  * start and stop hbugs web services
  * force submission of current status