]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

21 years agoadded architecture figure
Stefano Zacchiroli [Fri, 23 May 2003 11:09:54 +0000 (11:09 +0000)]
added architecture figure

21 years agoadded MONET's Math Obj Manager to conclusions
Stefano Zacchiroli [Fri, 23 May 2003 11:05:03 +0000 (11:05 +0000)]
added MONET's Math Obj Manager to conclusions

21 years agoadded multiple invocations of latex
Stefano Zacchiroli [Fri, 23 May 2003 11:04:31 +0000 (11:04 +0000)]
added multiple invocations of latex

21 years agoAdded all (???) the sections and their labels.
Claudio Sacerdoti Coen [Fri, 23 May 2003 09:56:15 +0000 (09:56 +0000)]
Added all (???) the sections and their labels.

21 years agoMinor improvements in the introduction.
Claudio Sacerdoti Coen [Fri, 23 May 2003 09:52:48 +0000 (09:52 +0000)]
Minor improvements in the introduction.

21 years ago* fix in optional argument for ocaml binding
Luca Padovani [Fri, 23 May 2003 09:24:55 +0000 (09:24 +0000)]
* fix in optional argument for ocaml binding
* fix in tml->mmlp stylehseet

21 years ago- Introduction changed.
Claudio Sacerdoti Coen [Thu, 22 May 2003 17:51:48 +0000 (17:51 +0000)]
- Introduction changed.
- Tasks assigned.

21 years agoed and draftstamp packages committed and activated
Claudio Sacerdoti Coen [Thu, 22 May 2003 16:05:12 +0000 (16:05 +0000)]
ed and draftstamp packages committed and activated

21 years agomathql query generator interface patched
Ferruccio Guidi [Thu, 22 May 2003 14:49:52 +0000 (14:49 +0000)]
mathql query generator interface patched

21 years agofirst checkin
Stefano Zacchiroli [Thu, 22 May 2003 07:33:44 +0000 (07:33 +0000)]
first checkin
- introduction
- outline
- auxiliary files

21 years agopatched
Ferruccio Guidi [Wed, 21 May 2003 11:00:31 +0000 (11:00 +0000)]
patched

21 years agoMathQL query generator: new interface
Ferruccio Guidi [Tue, 20 May 2003 14:52:11 +0000 (14:52 +0000)]
MathQL query generator: new interface

21 years agoSeveral changes:
Claudio Sacerdoti Coen [Thu, 15 May 2003 16:51:37 +0000 (16:51 +0000)]
Several changes:

1. the UWOBO_LOG_FILE environment variable semantics changed. It is now
   used in the following way: $UWOBO_LOG_FILE.pid.log
2. when the log file can not be opened, UWOBO used to crash. Instead,
   it now goes on and a nice error message is printed on the stderr
   (but, unfortunately, it is not given back to the user, since the
   error is raised in a new process and it can not be read back from
   the logfile!)

21 years agoThe semantics of the UWOBO_LOG variable has changed: the suffix ".log"
Claudio Sacerdoti Coen [Thu, 15 May 2003 16:31:05 +0000 (16:31 +0000)]
The semantics of the UWOBO_LOG variable has changed: the suffix ".log"
should not be in there any more.

21 years agoThe chmod ug+w in the all rule has been made non-critical.
Claudio Sacerdoti Coen [Thu, 15 May 2003 16:30:38 +0000 (16:30 +0000)]
The chmod ug+w in the all rule has been made non-critical.

21 years agoThis commit undoes part of the previous commit, where I mistakenly committed
Claudio Sacerdoti Coen [Thu, 15 May 2003 12:18:30 +0000 (12:18 +0000)]
This commit undoes part of the previous commit, where I mistakenly committed
parts of my laptop settings.

21 years agoNew: two methods have been added to kill UWOBO and to start a new session
Claudio Sacerdoti Coen [Thu, 15 May 2003 12:15:43 +0000 (12:15 +0000)]
New: two methods have been added to kill UWOBO and to start a new session
     (i.e. a new UWOBO process) listening on a given port)

21 years agoNew: two new methods added
Claudio Sacerdoti Coen [Thu, 15 May 2003 12:11:52 +0000 (12:11 +0000)]
New: two new methods added

* /newsession to create a new session on a given port (i.e. to fork a new
  UWOBO that starts listening on the new given port)
* /kill to ask an UWOBO to finish the execution

21 years agoMQueryInterpreter: interface updated
Ferruccio Guidi [Wed, 30 Apr 2003 13:56:57 +0000 (13:56 +0000)]
MQueryInterpreter: interface updated