]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years agoBug fixed: the value of parameters must be valid XPath string literals ==>
Claudio Sacerdoti Coen [Fri, 11 Jul 2003 10:01:05 +0000 (10:01 +0000)]
Bug fixed: the value of parameters must be valid XPath string literals ==>
they can not contain both ' and " (at least in Veillard interpretation, of
course ;-)

The fix applied consist in accepting parameters with only ' or only " inside
by quoting them using the opposite quote. As a consequence, variable
values with just 's inside are now handled correctly.

21 years agoprose patched
Ferruccio Guidi [Thu, 10 Jul 2003 14:38:34 +0000 (14:38 +0000)]
prose patched

21 years agolinks page added
Ferruccio Guidi [Thu, 10 Jul 2003 10:47:19 +0000 (10:47 +0000)]
links page added

21 years agoimplementation and whatsnew pages added
Ferruccio Guidi [Wed, 9 Jul 2003 16:33:36 +0000 (16:33 +0000)]
implementation and whatsnew pages added

21 years ago"backPointer" metadata enabled
Ferruccio Guidi [Thu, 3 Jul 2003 14:14:49 +0000 (14:14 +0000)]
"backPointer" metadata enabled

21 years agonew "light" implementation of intersection (compatible with the generator)
Ferruccio Guidi [Thu, 3 Jul 2003 10:55:47 +0000 (10:55 +0000)]
new "light" implementation of intersection (compatible with the generator)

21 years agorendering of "meet" patched
Ferruccio Guidi [Wed, 2 Jul 2003 17:34:09 +0000 (17:34 +0000)]
rendering of "meet" patched

21 years agoBug fixed: deselecting a constraint just forgot its depth.
Claudio Sacerdoti Coen [Wed, 2 Jul 2003 11:37:18 +0000 (11:37 +0000)]
Bug fixed: deselecting a constraint just forgot its depth.

21 years agomathql_generator: new constraint format (more type safe)
Ferruccio Guidi [Wed, 2 Jul 2003 11:01:34 +0000 (11:01 +0000)]
mathql_generator: new constraint format (more type safe)
mathql_test     : moved outside ocaml

21 years agoCtr+Backspace is now enabled. Used to perform "alternative" deletion.
Claudio Sacerdoti Coen [Wed, 2 Jul 2003 10:30:01 +0000 (10:30 +0000)]
Ctr+Backspace is now enabled. Used to perform "alternative" deletion.

21 years agoThe editor window now scrolls when the user exceeds the available space.
Claudio Sacerdoti Coen [Wed, 2 Jul 2003 10:24:38 +0000 (10:24 +0000)]
The editor window now scrolls when the user exceeds the available space.

21 years ago- DoubleTypeInference.does_not_occur exposed
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 15:25:38 +0000 (15:25 +0000)]
- DoubleTypeInference.does_not_occur exposed
- dummy bindings in Prods are no longer generated: arrows are now generated

21 years ago- changed changelog author to me (to GPG sign the package)
Stefano Zacchiroli [Tue, 1 Jul 2003 09:39:16 +0000 (09:39 +0000)]
- changed changelog author to me (to GPG sign the package)
- added dependencies on gmetadom >= 0.1.10-2 (so that the .pc is available)

21 years ago0.4.3-2
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 09:27:35 +0000 (09:27 +0000)]
0.4.3-2

21 years ago1. freeze/thaw added to reduce flickering due to selection changes
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 09:16:51 +0000 (09:16 +0000)]
1. freeze/thaw added to reduce flickering due to selection changes
2. SEMANTICA CHANGE: structural selection is no longer activated just
   before semantic selection

21 years agogtkmathview-config and gdome-config no longer used
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 09:15:52 +0000 (09:15 +0000)]
gtkmathview-config and gdome-config no longer used

21 years agodebian release 0.0.4-6
Stefano Zacchiroli [Tue, 1 Jul 2003 08:25:33 +0000 (08:25 +0000)]
debian release 0.0.4-6

21 years agomoved debhelper compatibility level to debian/compat
Stefano Zacchiroli [Tue, 1 Jul 2003 08:11:13 +0000 (08:11 +0000)]
moved debhelper compatibility level to debian/compat

21 years ago- default font size of the proof window lowered to 10
Claudio Sacerdoti Coen [Mon, 30 Jun 2003 13:52:58 +0000 (13:52 +0000)]
- default font size of the proof window lowered to 10
- the font size spinner is now initialized with the right value

21 years agomathql_interpreter: natile-galax package removed from Makefie and META
Ferruccio Guidi [Sun, 29 Jun 2003 18:28:58 +0000 (18:28 +0000)]
mathql_interpreter: natile-galax package removed from Makefie and META
mathql_generator  : MQueryLevels2.ml patched (namespaces removed from sorts)

21 years agoThe type of a LetIn is now a LetIn if and only if the bound variable really
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 17:18:18 +0000 (17:18 +0000)]
The type of a LetIn is now a LetIn if and only if the bound variable really
occurs.

21 years agoThe "Save proof" menu item is now activated when a finished proof is reopened.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 16:53:31 +0000 (16:53 +0000)]
The "Save proof" menu item is now activated when a finished proof is reopened.

21 years agoReindentation.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 15:37:53 +0000 (15:37 +0000)]
Reindentation.

21 years agoReloading bugged stylesheets no longer makes gTopLevel crash.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 13:51:55 +0000 (13:51 +0000)]
Reloading bugged stylesheets no longer makes gTopLevel crash.

21 years agoReload stylesheets menu entry added (under the Settings menu)
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 13:07:34 +0000 (13:07 +0000)]
Reload stylesheets menu entry added (under the Settings menu)

21 years ago...
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 12:34:44 +0000 (12:34 +0000)]
...

21 years agohttp://....#Prop shortened to Prop due to a bug (feature?) in the DB.
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 16:50:17 +0000 (16:50 +0000)]
http://....#Prop shortened to Prop due to a bug (feature?) in the DB.

21 years agorelativeDepth function removed (useful only for cooking)
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:59:50 +0000 (12:59 +0000)]
relativeDepth function removed (useful only for cooking)

21 years agoMetadata tools are now working correctly also over .body files.
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:48:03 +0000 (12:48 +0000)]
Metadata tools are now working correctly also over .body files.

21 years agoThe proof-checker should now be working also on .body files.
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:44:42 +0000 (12:44 +0000)]
The proof-checker should now be working also on .body files.

21 years agodropBodySuffix function added
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:43:58 +0000 (12:43 +0000)]
dropBodySuffix function added

21 years ago- Object URL link added
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:29:39 +0000 (12:29 +0000)]
- Object URL link added
- rethorical text changed

21 years agoPorted to the latest version of libhttp
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:14:18 +0000 (12:14 +0000)]
Ported to the latest version of libhttp

21 years agoadded tons of #include <cassert> to make latest gcc compiler happy
Stefano Zacchiroli [Wed, 25 Jun 2003 17:13:20 +0000 (17:13 +0000)]
added tons of #include <cassert> to make latest gcc compiler happy

21 years agopreliminar 0.0.3-2 debian release
Stefano Zacchiroli [Wed, 25 Jun 2003 16:39:12 +0000 (16:39 +0000)]
preliminar 0.0.3-2 debian release

21 years agoforward ported to use pkg-config
Stefano Zacchiroli [Wed, 25 Jun 2003 16:23:35 +0000 (16:23 +0000)]
forward ported to use pkg-config

21 years agoIt should have already been moved to ocaml/mathql_generator
Andrea Asperti [Wed, 25 Jun 2003 12:28:59 +0000 (12:28 +0000)]
It should have already been moved to ocaml/mathql_generator

21 years agoRemoved (it should have already been in ocaml/tactics)
Claudio Sacerdoti Coen [Wed, 25 Jun 2003 12:26:38 +0000 (12:26 +0000)]
Removed (it should have already been in ocaml/tactics)

21 years agoPorting to the latest version of PXP (1.1.94).
Claudio Sacerdoti Coen [Tue, 24 Jun 2003 12:17:02 +0000 (12:17 +0000)]
Porting to the latest version of PXP (1.1.94).

21 years agoNo longer in use.
Claudio Sacerdoti Coen [Tue, 24 Jun 2003 09:31:01 +0000 (09:31 +0000)]
No longer in use.

21 years agoBranch V7_3_new_exportation merged.
Claudio Sacerdoti Coen [Mon, 23 Jun 2003 16:10:58 +0000 (16:10 +0000)]
Branch V7_3_new_exportation merged.

21 years agoBranch V7_3_new_exportation merged.
Claudio Sacerdoti Coen [Mon, 23 Jun 2003 15:58:50 +0000 (15:58 +0000)]
Branch V7_3_new_exportation merged.

21 years ago- help method added
Claudio Sacerdoti Coen [Mon, 23 Jun 2003 14:31:45 +0000 (14:31 +0000)]
- help method added
- branch V7_3_new_exportation merged

21 years agostyles directory creation now works even if stylesheets and meta_stylesheets
Ferruccio Guidi [Fri, 20 Jun 2003 17:57:50 +0000 (17:57 +0000)]
styles directory creation now works even if stylesheets and meta_stylesheets
are symbolic links (as in my case)

21 years agoAuthor specification added in head comments;
Ferruccio Guidi [Fri, 20 Jun 2003 15:23:55 +0000 (15:23 +0000)]
Author specification added in head comments;
MQueryGenerator.builtin ready to be used

21 years ago...
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 14:27:23 +0000 (14:27 +0000)]
...

21 years agoInstallation instructions.
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 14:25:45 +0000 (14:25 +0000)]
Installation instructions.

21 years ago- script.sh added to the repository: you should change it to reflect your
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 14:24:00 +0000 (14:24 +0000)]
- script.sh added to the repository: you should change it to reflect your
  own settings
- the Makefile tries now to automatically build the styles directory, made
  only of hyperlinks to the styles in stylesheets and stylesheets/generated.
  Before doing make, you have to check out the stylesheets and meta_stylesheets
  repositories from the mowgli archive.
- added rootcontent.xsl which is the version used by gTopLevel until we find
  a better solution. You should change it to reflect your own settings.

21 years agoNew version 0.0.3:
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 12:06:51 +0000 (12:06 +0000)]
New version 0.0.3:
 - tml-litex.xsl was not installed
 - guiGTK.h did not include gdome.h
 - configure.ac was not correctly ported to pkg-config, since it still
   checked for the existence of the *-config executables for all the
   packages editex depends on. Fixed.

21 years ago* mquery_interpreter logging and debugging activated
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 17:54:03 +0000 (17:54 +0000)]
* mquery_interpreter logging and debugging activated
* bug fixed: the universe of the complete search pattern must exclude
  the InBody occurrences

21 years agoThe universe was the one of the complete search, not that of the
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 17:49:21 +0000 (17:49 +0000)]
The universe was the one of the complete search, not that of the
searchPatter (restricted to the conclusion).

21 years agoReindented
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 17:34:35 +0000 (17:34 +0000)]
Reindented

21 years agoMerge of the V7_3_new_exportation branch.
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 15:31:51 +0000 (15:31 +0000)]
Merge of the V7_3_new_exportation branch.

21 years agoremoved old -config script
Stefano Zacchiroli [Thu, 19 Jun 2003 15:28:41 +0000 (15:28 +0000)]
removed old -config script

21 years ago#include <cassert> patch
Stefano Zacchiroli [Thu, 19 Jun 2003 15:27:46 +0000 (15:27 +0000)]
#include <cassert> patch

21 years agodebian version 0.0.4-5
Stefano Zacchiroli [Thu, 19 Jun 2003 15:27:32 +0000 (15:27 +0000)]
debian version 0.0.4-5

21 years agoNew version 0.0.2:
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 15:25:33 +0000 (15:25 +0000)]
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

21 years ago* added pkg-config stuff
Luca Padovani [Thu, 19 Jun 2003 15:11:38 +0000 (15:11 +0000)]
* added pkg-config stuff

21 years agofixed autoconf variable @@ vs $()
Stefano Zacchiroli [Thu, 19 Jun 2003 15:00:50 +0000 (15:00 +0000)]
fixed autoconf variable @@ vs $()

21 years agoMathQL 1.3 ready for use
Ferruccio Guidi [Thu, 19 Jun 2003 14:37:12 +0000 (14:37 +0000)]
MathQL 1.3 ready for use

21 years agodebian version 0.4.3 (maybe, not tested)
Stefano Zacchiroli [Thu, 19 Jun 2003 14:30:24 +0000 (14:30 +0000)]
debian version 0.4.3 (maybe, not tested)

21 years ago* removed *-config script invocations, now using pkg-config
Luca Padovani [Thu, 19 Jun 2003 13:11:30 +0000 (13:11 +0000)]
* removed *-config script invocations, now using pkg-config

21 years agobumped version to 0.4.3
Stefano Zacchiroli [Thu, 19 Jun 2003 13:01:37 +0000 (13:01 +0000)]
bumped version to 0.4.3

21 years agoNo longer used.
Claudio Sacerdoti Coen [Wed, 18 Jun 2003 12:55:21 +0000 (12:55 +0000)]
No longer used.

21 years ago* added template for tml:s
Luca Padovani [Wed, 18 Jun 2003 12:53:24 +0000 (12:53 +0000)]
* added template for tml:s
* if the cursor is the empty string it is not produced

21 years ago- tabs removed
Claudio Sacerdoti Coen [Tue, 10 Jun 2003 14:59:38 +0000 (14:59 +0000)]
- tabs removed
- "\" correctly quoted in strings
- in case of self-loops, the process diverged. Self-loops are now
  ignored during parsing.

21 years agofindlib introduced
Claudio Sacerdoti Coen [Tue, 10 Jun 2003 14:44:39 +0000 (14:44 +0000)]
findlib introduced

21 years ago* the non-empty cursor is now generated
Luca Padovani [Wed, 4 Jun 2003 13:00:55 +0000 (13:00 +0000)]
* the non-empty cursor is now generated

21 years ago* patched wrong commit (perhaps...)
Luca Padovani [Wed, 4 Jun 2003 10:50:10 +0000 (10:50 +0000)]
* patched wrong commit (perhaps...)

21 years agonew syntax for "property" enabled:
Ferruccio Guidi [Sat, 31 May 2003 18:59:06 +0000 (18:59 +0000)]
new syntax for "property" enabled:
 now many "isfalse" clauses are accepted

21 years agofinal ispell
Claudio Sacerdoti Coen [Fri, 30 May 2003 17:17:58 +0000 (17:17 +0000)]
final ispell

21 years agoMinor modifications to the new session.
Claudio Sacerdoti Coen [Fri, 30 May 2003 17:13:42 +0000 (17:13 +0000)]
Minor modifications to the new session.

21 years ago...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:20:28 +0000 (15:20 +0000)]
...

21 years ago...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:18:31 +0000 (15:18 +0000)]
...

21 years agocolor ==> gray
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:18:26 +0000 (15:18 +0000)]
color ==> gray

21 years ago...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:09:45 +0000 (15:09 +0000)]
...

21 years agoNew session (the H-Bugs interactive session).
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:08:25 +0000 (15:08 +0000)]
New session (the H-Bugs interactive session).

21 years agodraft review
Stefano Zacchiroli [Thu, 29 May 2003 21:14:06 +0000 (21:14 +0000)]
draft review

21 years agoNew ispell.
Claudio Sacerdoti Coen [Thu, 29 May 2003 20:52:06 +0000 (20:52 +0000)]
New ispell.

21 years agoSeveral other small changes here and there.
Claudio Sacerdoti Coen [Thu, 29 May 2003 20:48:45 +0000 (20:48 +0000)]
Several other small changes here and there.

21 years ago...
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:59:37 +0000 (17:59 +0000)]
...

21 years agothread handling reviewed
Stefano Zacchiroli [Thu, 29 May 2003 17:57:06 +0000 (17:57 +0000)]
thread handling reviewed

21 years agoFigure moved to the next page.
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:50:52 +0000 (17:50 +0000)]
Figure moved to the next page.

21 years agoSeveral editor notes resolved.
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:48:22 +0000 (17:48 +0000)]
Several editor notes resolved.

21 years agoEverything Ispell-ed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 13:43:15 +0000 (13:43 +0000)]
Everything Ispell-ed.

21 years agoOther references added.
Claudio Sacerdoti Coen [Thu, 29 May 2003 13:31:42 +0000 (13:31 +0000)]
Other references added.
An old part removed.

21 years agoA new references.
Claudio Sacerdoti Coen [Thu, 29 May 2003 12:26:57 +0000 (12:26 +0000)]
A new references.

21 years agoMany references committed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 12:22:28 +0000 (12:22 +0000)]
Many references committed.

21 years agoSome editor notes closed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 11:34:30 +0000 (11:34 +0000)]
Some editor notes closed.

21 years agoLots of small changes in the text.
Claudio Sacerdoti Coen [Thu, 29 May 2003 11:29:39 +0000 (11:29 +0000)]
Lots of small changes in the text.

21 years agoextended syntax for add
Ferruccio Guidi [Wed, 28 May 2003 13:57:33 +0000 (13:57 +0000)]
extended syntax for add

21 years ago- several changes in all the parts that made comparisons with MONET
Claudio Sacerdoti Coen [Wed, 28 May 2003 12:01:43 +0000 (12:01 +0000)]
- several changes in all the parts that made comparisons with MONET
- added a few sentences in the conclusions section

21 years agoadded web-services' interfaces image
Stefano Zacchiroli [Wed, 28 May 2003 06:58:59 +0000 (06:58 +0000)]
added web-services' interfaces image

21 years ago- reviewed latest CSC'comments
Stefano Zacchiroli [Wed, 28 May 2003 06:58:47 +0000 (06:58 +0000)]
- reviewed latest CSC'comments
- added future works
- added an image

21 years agosite updated
Ferruccio Guidi [Tue, 27 May 2003 13:24:52 +0000 (13:24 +0000)]
site updated

21 years agoSeveral small changes to the parts committed by Zack.
Claudio Sacerdoti Coen [Tue, 27 May 2003 13:11:44 +0000 (13:11 +0000)]
Several small changes to the parts committed by Zack.

21 years agoadded status.eps
Stefano Zacchiroli [Mon, 26 May 2003 12:44:47 +0000 (12:44 +0000)]
added status.eps

21 years agowritten section 3
Stefano Zacchiroli [Mon, 26 May 2003 07:53:49 +0000 (07:53 +0000)]
written section 3

21 years agoFirst part of the chapter about tutors. The automatic generation part is
Claudio Sacerdoti Coen [Fri, 23 May 2003 11:50:12 +0000 (11:50 +0000)]
First part of the chapter about tutors. The automatic generation part is
still missing.

21 years ago- (badly) written section 2 (Architecture)
Stefano Zacchiroli [Fri, 23 May 2003 11:11:42 +0000 (11:11 +0000)]
- (badly) written section 2 (Architecture)
- removed old oldparts in introduction, added some ednotes