]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years ago* first snapshot
Luca Padovani [Tue, 15 Jul 2003 14:54:22 +0000 (14:54 +0000)]
* first snapshot

21 years agomerged CSC's typos squashing
Stefano Zacchiroli [Tue, 15 Jul 2003 14:50:42 +0000 (14:50 +0000)]
merged CSC's typos squashing

21 years agofixed "s" typos
Stefano Zacchiroli [Tue, 15 Jul 2003 10:14:24 +0000 (10:14 +0000)]
fixed "s" typos

21 years agodescription for "Irene Schena" added in authors.html
Ferruccio Guidi [Tue, 15 Jul 2003 09:17:59 +0000 (09:17 +0000)]
description for "Irene Schena" added in authors.html

21 years agowrapped libxslt stylesheet application inside an ocaml blocking section
Stefano Zacchiroli [Tue, 15 Jul 2003 06:36:25 +0000 (06:36 +0000)]
wrapped libxslt stylesheet application inside an ocaml blocking section
so that ocaml exceptions, signals and other asynchronous stuff could be
handled in the meantime

21 years agobumped version to 0.0.5
Stefano Zacchiroli [Tue, 15 Jul 2003 06:35:42 +0000 (06:35 +0000)]
bumped version to 0.0.5

21 years agoTowards the camera ready.
Claudio Sacerdoti Coen [Mon, 14 Jul 2003 17:05:15 +0000 (17:05 +0000)]
Towards the camera ready.

21 years agodebian release 0.0.4-7
Stefano Zacchiroli [Mon, 14 Jul 2003 09:19:54 +0000 (09:19 +0000)]
debian release 0.0.4-7

21 years agodebian release 0.4.3-3
Stefano Zacchiroli [Sat, 12 Jul 2003 12:18:09 +0000 (12:18 +0000)]
debian release 0.4.3-3

21 years agoreordered link order
Stefano Zacchiroli [Fri, 11 Jul 2003 13:29:58 +0000 (13:29 +0000)]
reordered link order

21 years agoVersion dumped.
Claudio Sacerdoti Coen [Fri, 11 Jul 2003 10:05:10 +0000 (10:05 +0000)]
Version dumped.

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.