]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Wed, 2 Jul 2003 10:30:01 +0000 (10:30 +0000)]
Ctr+Backspace is now enabled. Used to perform "alternative" deletion.
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.
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
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)
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 09:27:35 +0000 (09:27 +0000)]
0.4.3-2
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
Claudio Sacerdoti Coen [Tue, 1 Jul 2003 09:15:52 +0000 (09:15 +0000)]
gtkmathview-config and gdome-config no longer used
Stefano Zacchiroli [Tue, 1 Jul 2003 08:25:33 +0000 (08:25 +0000)]
debian release 0.0.4-6
Stefano Zacchiroli [Tue, 1 Jul 2003 08:11:13 +0000 (08:11 +0000)]
moved debhelper compatibility level to debian/compat
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
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)
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.
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.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 15:37:53 +0000 (15:37 +0000)]
Reindentation.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 13:51:55 +0000 (13:51 +0000)]
Reloading bugged stylesheets no longer makes gTopLevel crash.
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 13:07:34 +0000 (13:07 +0000)]
Reload stylesheets menu entry added (under the Settings menu)
Claudio Sacerdoti Coen [Fri, 27 Jun 2003 12:34:44 +0000 (12:34 +0000)]
...
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.
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:59:50 +0000 (12:59 +0000)]
relativeDepth function removed (useful only for cooking)
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:48:03 +0000 (12:48 +0000)]
Metadata tools are now working correctly also over .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.
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:43:58 +0000 (12:43 +0000)]
dropBodySuffix function added
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:29:39 +0000 (12:29 +0000)]
- Object URL link added
- rethorical text changed
Claudio Sacerdoti Coen [Thu, 26 Jun 2003 12:14:18 +0000 (12:14 +0000)]
Ported to the latest version of libhttp
Stefano Zacchiroli [Wed, 25 Jun 2003 17:13:20 +0000 (17:13 +0000)]
added tons of #include <cassert> to make latest gcc compiler happy
Stefano Zacchiroli [Wed, 25 Jun 2003 16:39:12 +0000 (16:39 +0000)]
preliminar 0.0.3-2 debian release
Stefano Zacchiroli [Wed, 25 Jun 2003 16:23:35 +0000 (16:23 +0000)]
forward ported to use pkg-config
Andrea Asperti [Wed, 25 Jun 2003 12:28:59 +0000 (12:28 +0000)]
It should have already been moved to ocaml/mathql_generator
Claudio Sacerdoti Coen [Wed, 25 Jun 2003 12:26:38 +0000 (12:26 +0000)]
Removed (it should have already been in ocaml/tactics)
Claudio Sacerdoti Coen [Tue, 24 Jun 2003 12:17:02 +0000 (12:17 +0000)]
Porting to the latest version of PXP (1.1.94).
Claudio Sacerdoti Coen [Tue, 24 Jun 2003 09:31:01 +0000 (09:31 +0000)]
No longer in use.
Claudio Sacerdoti Coen [Mon, 23 Jun 2003 16:10:58 +0000 (16:10 +0000)]
Branch 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.
Claudio Sacerdoti Coen [Mon, 23 Jun 2003 14:31:45 +0000 (14:31 +0000)]
- help method added
- branch V7_3_new_exportation merged
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)
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
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 14:27:23 +0000 (14:27 +0000)]
...
Claudio Sacerdoti Coen [Fri, 20 Jun 2003 14:25:45 +0000 (14:25 +0000)]
Installation instructions.
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.
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.
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
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).
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 17:34:35 +0000 (17:34 +0000)]
Reindented
Claudio Sacerdoti Coen [Thu, 19 Jun 2003 15:31:51 +0000 (15:31 +0000)]
Merge of the V7_3_new_exportation branch.
Stefano Zacchiroli [Thu, 19 Jun 2003 15:28:41 +0000 (15:28 +0000)]
removed old -config script
Stefano Zacchiroli [Thu, 19 Jun 2003 15:27:46 +0000 (15:27 +0000)]
#include <cassert> patch
Stefano Zacchiroli [Thu, 19 Jun 2003 15:27:32 +0000 (15:27 +0000)]
debian version 0.0.4-5
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
Luca Padovani [Thu, 19 Jun 2003 15:11:38 +0000 (15:11 +0000)]
* added pkg-config stuff
Stefano Zacchiroli [Thu, 19 Jun 2003 15:00:50 +0000 (15:00 +0000)]
fixed autoconf variable @@ vs $()
Ferruccio Guidi [Thu, 19 Jun 2003 14:37:12 +0000 (14:37 +0000)]
MathQL 1.3 ready for use
Stefano Zacchiroli [Thu, 19 Jun 2003 14:30:24 +0000 (14:30 +0000)]
debian version 0.4.3 (maybe, not tested)
Luca Padovani [Thu, 19 Jun 2003 13:11:30 +0000 (13:11 +0000)]
* removed *-config script invocations, now using pkg-config
Stefano Zacchiroli [Thu, 19 Jun 2003 13:01:37 +0000 (13:01 +0000)]
bumped version to 0.4.3
Claudio Sacerdoti Coen [Wed, 18 Jun 2003 12:55:21 +0000 (12:55 +0000)]
No longer used.
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
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.
Claudio Sacerdoti Coen [Tue, 10 Jun 2003 14:44:39 +0000 (14:44 +0000)]
findlib introduced
Luca Padovani [Wed, 4 Jun 2003 13:00:55 +0000 (13:00 +0000)]
* the non-empty cursor is now generated
Luca Padovani [Wed, 4 Jun 2003 10:50:10 +0000 (10:50 +0000)]
* patched wrong commit (perhaps...)
Ferruccio Guidi [Sat, 31 May 2003 18:59:06 +0000 (18:59 +0000)]
new syntax for "property" enabled:
now many "isfalse" clauses are accepted
Claudio Sacerdoti Coen [Fri, 30 May 2003 17:17:58 +0000 (17:17 +0000)]
final ispell
Claudio Sacerdoti Coen [Fri, 30 May 2003 17:13:42 +0000 (17:13 +0000)]
Minor modifications to the new session.
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:20:28 +0000 (15:20 +0000)]
...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:18:31 +0000 (15:18 +0000)]
...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:18:26 +0000 (15:18 +0000)]
color ==> gray
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:09:45 +0000 (15:09 +0000)]
...
Claudio Sacerdoti Coen [Fri, 30 May 2003 15:08:25 +0000 (15:08 +0000)]
New session (the H-Bugs interactive session).
Stefano Zacchiroli [Thu, 29 May 2003 21:14:06 +0000 (21:14 +0000)]
draft review
Claudio Sacerdoti Coen [Thu, 29 May 2003 20:52:06 +0000 (20:52 +0000)]
New ispell.
Claudio Sacerdoti Coen [Thu, 29 May 2003 20:48:45 +0000 (20:48 +0000)]
Several other small changes here and there.
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:59:37 +0000 (17:59 +0000)]
...
Stefano Zacchiroli [Thu, 29 May 2003 17:57:06 +0000 (17:57 +0000)]
thread handling reviewed
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:50:52 +0000 (17:50 +0000)]
Figure moved to the next page.
Claudio Sacerdoti Coen [Thu, 29 May 2003 17:48:22 +0000 (17:48 +0000)]
Several editor notes resolved.
Claudio Sacerdoti Coen [Thu, 29 May 2003 13:43:15 +0000 (13:43 +0000)]
Everything Ispell-ed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 13:31:42 +0000 (13:31 +0000)]
Other references added.
An old part removed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 12:26:57 +0000 (12:26 +0000)]
A new references.
Claudio Sacerdoti Coen [Thu, 29 May 2003 12:22:28 +0000 (12:22 +0000)]
Many references committed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 11:34:30 +0000 (11:34 +0000)]
Some editor notes closed.
Claudio Sacerdoti Coen [Thu, 29 May 2003 11:29:39 +0000 (11:29 +0000)]
Lots of small changes in the text.
Ferruccio Guidi [Wed, 28 May 2003 13:57:33 +0000 (13:57 +0000)]
extended syntax for add
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
Stefano Zacchiroli [Wed, 28 May 2003 06:58:59 +0000 (06:58 +0000)]
added web-services' interfaces image
Stefano Zacchiroli [Wed, 28 May 2003 06:58:47 +0000 (06:58 +0000)]
- reviewed latest CSC'comments
- added future works
- added an image
Ferruccio Guidi [Tue, 27 May 2003 13:24:52 +0000 (13:24 +0000)]
site updated
Claudio Sacerdoti Coen [Tue, 27 May 2003 13:11:44 +0000 (13:11 +0000)]
Several small changes to the parts committed by Zack.
Stefano Zacchiroli [Mon, 26 May 2003 12:44:47 +0000 (12:44 +0000)]
added status.eps
Stefano Zacchiroli [Mon, 26 May 2003 07:53:49 +0000 (07:53 +0000)]
written section 3
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.
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
Stefano Zacchiroli [Fri, 23 May 2003 11:09:54 +0000 (11:09 +0000)]
added architecture figure
Stefano Zacchiroli [Fri, 23 May 2003 11:05:03 +0000 (11:05 +0000)]
added MONET's Math Obj Manager to conclusions
Stefano Zacchiroli [Fri, 23 May 2003 11:04:31 +0000 (11:04 +0000)]
added multiple invocations of latex
Claudio Sacerdoti Coen [Fri, 23 May 2003 09:56:15 +0000 (09:56 +0000)]
Added all (???) the sections and their labels.
Claudio Sacerdoti Coen [Fri, 23 May 2003 09:52:48 +0000 (09:52 +0000)]
Minor improvements in the introduction.
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
Claudio Sacerdoti Coen [Thu, 22 May 2003 17:51:48 +0000 (17:51 +0000)]
- Introduction changed.
- Tasks assigned.
Claudio Sacerdoti Coen [Thu, 22 May 2003 16:05:12 +0000 (16:05 +0000)]
ed and draftstamp packages committed and activated
Ferruccio Guidi [Thu, 22 May 2003 14:49:52 +0000 (14:49 +0000)]
mathql query generator interface patched