patched

first version

This commit was manufactured by cvs2svn to create branch 'mathql_1_4'.

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

added support for X11 clipboard pasting with CTRL-V shortcut

added methods to start/stop web services

added eqT's macro

scrollbars added & control structure screated

fixed typo in eqT's URI

CGLocateInductive patched

added the support for the "Locate Inductive Principles" query

* removed wrong unref

* added test .html file for mozilla plugin

* a few adjustments and debugging messages added
* works as a component in mozilla

Closed induction cases are now pointers to the acontext/conclusion ==>
they are now perforated correctly.

* added first version of persist stream implementation (not yet working)
* added test for property bag (read-only for now)

"proof of X" closed mactions were not selectable

1. folded maction are now selectable
2. metavariable occurrences are now displayed together with their
   substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order

* mime type updated

- support for comments added in mathql_db_map.txt

Unuseful id removed from hypothesis.

- information about the database map added in whatsnew.html
- spell checked

Eta fixing for MTCases added (that meant to recursively pass around the
context).

All the ids are now generated by gen_id. (Some of them were previously based
on the acic ids).

* quite a lot of patches in the building stuff

new links added

Added method FalseInd

Added method "FalseInd".

Prefixes introduced for the generated ids/xrefs. Example:
 "proof:" for proofs
 "decl:"  for declarations
 ...

- the mathql interpreter is not helm-dependent any more
- fixed a bug in the "match conclusion" query of the search engine
- gTopLevel/Makefile improved

Spurious files removed.

"(" moved from Mtext to Mo. Spaces removed.

Added method AndInd.

Added Method "exists".