]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agohandle multiple href
Stefano Zacchiroli [Mon, 25 Jul 2005 10:15:36 +0000 (10:15 +0000)]
handle multiple href

19 years agoadded split
Stefano Zacchiroli [Mon, 25 Jul 2005 10:15:04 +0000 (10:15 +0000)]
added split

19 years agoimplemented transformations on top of notation code
Stefano Zacchiroli [Mon, 25 Jul 2005 10:14:34 +0000 (10:14 +0000)]
implemented transformations on top of notation code

19 years agomoved add_xml_declaration here
Stefano Zacchiroli [Mon, 25 Jul 2005 10:13:46 +0000 (10:13 +0000)]
moved add_xml_declaration here

19 years ago- addded unicode_of_tex
Stefano Zacchiroli [Mon, 25 Jul 2005 10:13:30 +0000 (10:13 +0000)]
- addded unicode_of_tex
- added \neq macro

19 years agoParamodulation initialized.
Claudio Sacerdoti Coen [Mon, 25 Jul 2005 09:40:08 +0000 (09:40 +0000)]
Paramodulation initialized.

19 years ago...
Claudio Sacerdoti Coen [Mon, 25 Jul 2005 08:54:23 +0000 (08:54 +0000)]
...

19 years agoadded optional "paramodulation" parameter to auto to turn on paramodulation
Alberto Griggio [Fri, 22 Jul 2005 17:53:47 +0000 (17:53 +0000)]
added optional "paramodulation" parameter to auto to turn on paramodulation

19 years agoadded optional "paramodulation" parameter to auto to turn on paramodulation
Alberto Griggio [Fri, 22 Jul 2005 17:29:00 +0000 (17:29 +0000)]
added optional "paramodulation" parameter to auto to turn on paramodulation

19 years ago- better exception handling
Alberto Griggio [Fri, 22 Jul 2005 17:27:40 +0000 (17:27 +0000)]
- better exception handling
- compiled with -pack to get a Paramodulation namespace
- fixed a bug in Inference.unification_simple

19 years agoWhen matita is started on a non-existent file, it avoids creating it
Claudio Sacerdoti Coen [Fri, 22 Jul 2005 16:51:18 +0000 (16:51 +0000)]
When matita is started on a non-existent file, it avoids creating it
immediately!

19 years agoOriginal semantics of a now almost random piece of code restored.
Claudio Sacerdoti Coen [Fri, 22 Jul 2005 16:01:13 +0000 (16:01 +0000)]
Original semantics of a now almost random piece of code restored.
Fixes the automatic compilation of .moos when matita is started from a directory
that is not the root of a library.

19 years agoAn object should be removed from disk (i.e. from the Getter scope) _before_ removing it
Andrea Asperti [Fri, 22 Jul 2005 14:33:53 +0000 (14:33 +0000)]
An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
from the environment.

19 years agoCicEnvironment.remove did not remove the object from the unchecked_list.
Andrea Asperti [Fri, 22 Jul 2005 14:33:09 +0000 (14:33 +0000)]
CicEnvironment.remove did not remove the object from the unchecked_list.

19 years agofix
Enrico Tassi [Fri, 22 Jul 2005 14:13:26 +0000 (14:13 +0000)]
fix

19 years agoRemoved debugging print.
Andrea Asperti [Fri, 22 Jul 2005 13:54:08 +0000 (13:54 +0000)]
Removed debugging print.

19 years agomatitaclean all now destroys the .matita/xml directory
Claudio Sacerdoti Coen [Fri, 22 Jul 2005 13:43:21 +0000 (13:43 +0000)]
matitaclean all now destroys the .matita/xml directory

19 years agoBig changes:
Claudio Sacerdoti Coen [Fri, 22 Jul 2005 13:29:52 +0000 (13:29 +0000)]
Big changes:
 1. the .moo files are now kept in the logical structure (i.e. in .matita/xml/*)
 2. matitaclean is now able to correctly remove all the .moo files
 3. the compilation target in library and tests is now foo.mo (it used to be
    foo.moo) and it is PHONY

19 years agoadd_obj is ATOMIC
Enrico Tassi [Fri, 22 Jul 2005 11:46:25 +0000 (11:46 +0000)]
add_obj is ATOMIC

19 years agosome prerr to better understand the mkdir -p error
Enrico Tassi [Fri, 22 Jul 2005 11:46:00 +0000 (11:46 +0000)]
some prerr to better understand the mkdir -p error

19 years agoadded env content debug print
Enrico Tassi [Fri, 22 Jul 2005 11:45:35 +0000 (11:45 +0000)]
added env content debug print

19 years ago...
Claudio Sacerdoti Coen [Fri, 22 Jul 2005 08:47:10 +0000 (08:47 +0000)]
...

19 years agoadded some typechecks to avoid using equations with the wrong type
Alberto Griggio [Thu, 21 Jul 2005 22:28:31 +0000 (22:28 +0000)]
added some typechecks to avoid using equations with the wrong type

19 years agodependencies
Alberto Griggio [Thu, 21 Jul 2005 21:38:36 +0000 (21:38 +0000)]
dependencies

19 years agoremoved .depend from .cvsignore
Alberto Griggio [Thu, 21 Jul 2005 21:38:11 +0000 (21:38 +0000)]
removed .depend from .cvsignore

19 years agoadded some typechecks to avoid using equations with the wrong type
Alberto Griggio [Thu, 21 Jul 2005 21:37:52 +0000 (21:37 +0000)]
added some typechecks to avoid using equations with the wrong type

19 years agoadded CicNotation.load_notation call to disambiguate terms
Alberto Griggio [Thu, 21 Jul 2005 20:40:10 +0000 (20:40 +0000)]
added CicNotation.load_notation call to disambiguate terms

19 years agoif paramodulation fails, go on with the normal auto...
Alberto Griggio [Thu, 21 Jul 2005 20:34:55 +0000 (20:34 +0000)]
if paramodulation fails, go on with the normal auto...

19 years agoBug fixed: LICENSE and AUTHORS were searched in the current dir :-(
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 16:37:34 +0000 (16:37 +0000)]
Bug fixed: LICENSE and AUTHORS were searched in the current dir :-(

19 years ago...
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 16:32:50 +0000 (16:32 +0000)]
...

19 years agoRegression fixed: goto used to stop (again!) to the new cursor position when
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 16:32:20 +0000 (16:32 +0000)]
Regression fixed: goto used to stop (again!) to the new cursor position when
the user clicks somewhere. The source of the regression was the difficulty of
remembering the position of the marks while the text is modified (by automatic
insertion of aliases). Solved by using ad-hoc temporary marks in place of
iterators (first version tried) and offsets (most recent version tried).

19 years ago...
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 16:02:41 +0000 (16:02 +0000)]
...

19 years ago...
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 15:41:36 +0000 (15:41 +0000)]
...

19 years ago...
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 15:15:18 +0000 (15:15 +0000)]
...

19 years agoS_pred moved from Z/times.ma to nat/orders.ma
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 14:34:17 +0000 (14:34 +0000)]
S_pred moved from Z/times.ma to nat/orders.ma

19 years agoMatitaSync.remove must remove the objects also from the environment.
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 12:42:58 +0000 (12:42 +0000)]
MatitaSync.remove must remove the objects also from the environment.
This fixes the following bug: in matita open a file B that depends on A
(that gets loaded in the environment); then switch to A without exiting
matita. It is now impossible to re-compile A.

19 years agoremoved old broken code
Alberto Griggio [Thu, 21 Jul 2005 12:19:34 +0000 (12:19 +0000)]
removed old broken code

19 years agointegration with paramodulation
Alberto Griggio [Thu, 21 Jul 2005 11:53:48 +0000 (11:53 +0000)]
integration with paramodulation

19 years agointegration with paramodulation
Alberto Griggio [Thu, 21 Jul 2005 11:48:42 +0000 (11:48 +0000)]
integration with paramodulation

19 years agomodifications/fixes for the integration with auto
Alberto Griggio [Thu, 21 Jul 2005 11:47:50 +0000 (11:47 +0000)]
modifications/fixes for the integration with auto

19 years agoentry point of the stand-alone saturate
Alberto Griggio [Thu, 21 Jul 2005 11:45:58 +0000 (11:45 +0000)]
entry point of the stand-alone saturate

19 years agoadded paramodulation package
Alberto Griggio [Thu, 21 Jul 2005 11:44:33 +0000 (11:44 +0000)]
added paramodulation package

19 years agoComment "comments" removed from the outbox :-)
Claudio Sacerdoti Coen [Thu, 21 Jul 2005 11:10:30 +0000 (11:10 +0000)]
Comment "comments" removed from the outbox :-)

19 years agoBetter tooltips.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:41:31 +0000 (16:41 +0000)]
Better tooltips.

19 years agoTooltip removed.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:38:17 +0000 (16:38 +0000)]
Tooltip removed.

19 years ago...
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:34:12 +0000 (16:34 +0000)]
...

19 years agoView tactics bar ==> Show tactics bar
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:32:12 +0000 (16:32 +0000)]
View tactics bar ==> Show tactics bar

19 years ago...
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:28:48 +0000 (16:28 +0000)]
...

19 years agoAfter a goto the focus is now grabbed back by the insertion window.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:27:40 +0000 (16:27 +0000)]
After a goto the focus is now grabbed back by the insertion window.

19 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:25:32 +0000 (16:25 +0000)]
Debugging code commented out.

19 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:19:53 +0000 (16:19 +0000)]
Debugging code commented out.

19 years agoAccording to the Gnome Interface Guidelines the Help menu must be aliged
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:18:10 +0000 (16:18 +0000)]
According to the Gnome Interface Guidelines the Help menu must be aliged
as the other ones. It should not be all alone on the very right of the screen.

19 years ago...
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:14:36 +0000 (16:14 +0000)]
...

19 years agoNew files AUTHORS and LICENSE.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 16:13:24 +0000 (16:13 +0000)]
New files AUTHORS and LICENSE.
New about dialog box (automatically generated according to the Gnome Interface
Guidelines). The dialog box is filled with the informations from AUTHORS and
LICENSE.

19 years agoEmpty Box.Text changed to Box.smallskip.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 15:00:50 +0000 (15:00 +0000)]
Empty Box.Text changed to Box.smallskip.

19 years agoSeveral interface improvements here and there.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 14:11:53 +0000 (14:11 +0000)]
Several interface improvements here and there.
The interface is now closer to the Gnome Interface Guidelines.

19 years agobetter handling of backgroud compiler process
Enrico Tassi [Wed, 20 Jul 2005 13:51:30 +0000 (13:51 +0000)]
better handling of backgroud compiler process

19 years agoNew target cleantests.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 13:37:47 +0000 (13:37 +0000)]
New target cleantests.

19 years agoPretty printing of the disambiguation environment no longer ends in \n.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 13:37:04 +0000 (13:37 +0000)]
Pretty printing of the disambiguation environment no longer ends in \n.

19 years agoNicer handling of automatic text insertion.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 13:24:23 +0000 (13:24 +0000)]
Nicer handling of automatic text insertion.

19 years agoA "\n" is now prepended to the aliases that are inserted (to avoid the
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 13:18:36 +0000 (13:18 +0000)]
A "\n" is now prepended to the aliases that are inserted (to avoid the
creation of horrible long lines).

19 years agoBug fixed: we used to use iterators on a text that was modified, making
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 13:15:02 +0000 (13:15 +0000)]
Bug fixed: we used to use iterators on a text that was modified, making
Gtk raise non-critical erros.

19 years agofixed typo in 'leq interpretation uri which enable nice rendering of
Stefano Zacchiroli [Wed, 20 Jul 2005 12:49:37 +0000 (12:49 +0000)]
fixed typo in 'leq interpretation uri which enable nice rendering of
coq's le predicate

19 years ago...
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 12:48:44 +0000 (12:48 +0000)]
...

19 years ago...
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 12:48:09 +0000 (12:48 +0000)]
...

19 years agoUndo/Redo in the popup menu are now working correctly.
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 12:46:25 +0000 (12:46 +0000)]
Undo/Redo in the popup menu are now working correctly.

19 years agoRedo fixed with a strategy similar (but not equal) to the one for undo:
Claudio Sacerdoti Coen [Wed, 20 Jul 2005 08:19:33 +0000 (08:19 +0000)]
Redo fixed with a strategy similar (but not equal) to the one for undo:
1. we save the position of all the marks
2. we redo
3. we undo
4. we save the position of the cursor after the undo
5. if necessary, we restore the initial position of all the marks,
   we move the cursor to its position after the undo and then we goto
6. we redo

19 years agoAssert false removed (although conceptually correct).
Andrea Asperti [Wed, 20 Jul 2005 07:22:49 +0000 (07:22 +0000)]
Assert false removed (although conceptually correct).
The problem isgenerating names during the refinement of incomplete terms;
the right solution would be to generate names only AFTER refinement.

19 years agoUnuseful code removed.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 17:24:48 +0000 (17:24 +0000)]
Unuseful code removed.

19 years ago...
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 17:24:42 +0000 (17:24 +0000)]
...

19 years agofixed file descriptor leak
Stefano Zacchiroli [Tue, 19 Jul 2005 17:24:41 +0000 (17:24 +0000)]
fixed file descriptor leak

19 years agouse safe_remove to remove files instead of Unix.unlink
Stefano Zacchiroli [Tue, 19 Jul 2005 17:24:06 +0000 (17:24 +0000)]
use safe_remove to remove files instead of Unix.unlink

19 years agosorted cicBrowser's listings
Stefano Zacchiroli [Tue, 19 Jul 2005 17:23:35 +0000 (17:23 +0000)]
sorted cicBrowser's listings

19 years agoBug fix: undo now respects the locked area.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 17:22:14 +0000 (17:22 +0000)]
Bug fix: undo now respects the locked area.
Algorithm to fix the bug:
 1. save the status of all the marks
 2. undo
 3. save the status of the cursor after the undo
 4. redo
 5. restore the status of all the marks
 6. if necessary, move the cursor back to its position after the undo
    and perform a goto to unlock the area
 7. perform the undo again

The same algorithm should be applied again to the redo operation!

19 years agoNew menus Undo/Redo (bugged), Cut/Copy/Paste/Delete.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 16:00:06 +0000 (16:00 +0000)]
New menus Undo/Redo (bugged), Cut/Copy/Paste/Delete.

19 years agoblocked undo of authomatic text (template)
Enrico Tassi [Tue, 19 Jul 2005 14:15:25 +0000 (14:15 +0000)]
blocked undo of authomatic text (template)

19 years agoA tab converted to spaces as it should be.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 14:00:58 +0000 (14:00 +0000)]
A tab converted to spaces as it should be.

19 years agomessage if the duplicate check may take too long
Enrico Tassi [Tue, 19 Jul 2005 13:25:36 +0000 (13:25 +0000)]
message if the duplicate check may take too long

19 years agomatitac now automatically cleans a non empty baseuri
Enrico Tassi [Tue, 19 Jul 2005 13:20:45 +0000 (13:20 +0000)]
matitac now automatically cleans a non empty baseuri

19 years ago...
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 13:11:27 +0000 (13:11 +0000)]
...

19 years agoCtrl^D in matitatop fixed (was broken by the new parser of Zack and Luca)
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 13:10:06 +0000 (13:10 +0000)]
Ctrl^D in matitatop fixed (was broken by the new parser of Zack and Luca)

19 years ago...
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 12:59:27 +0000 (12:59 +0000)]
...

19 years agoMissing case (Cast) implemented.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 12:38:38 +0000 (12:38 +0000)]
Missing case (Cast) implemented.

19 years agoNew naming scheme (by Andrea).
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:58:44 +0000 (11:58 +0000)]
New naming scheme (by Andrea).

19 years agoNew naming scheme by Andrea.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:55:15 +0000 (11:55 +0000)]
New naming scheme by Andrea.

19 years agopatched
Ferruccio Guidi [Tue, 19 Jul 2005 11:46:10 +0000 (11:46 +0000)]
patched

19 years agoBench fixed.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:39:19 +0000 (11:39 +0000)]
Bench fixed.

19 years agoUsed to left temporary file if something failed.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:34:41 +0000 (11:34 +0000)]
Used to left temporary file if something failed.

19 years agoMany bugs in the Makefile fixed.
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:33:32 +0000 (11:33 +0000)]
Many bugs in the Makefile fixed.
make inside library/tests now stops at the first error
make tests{,.opt} goes on trying to compile everything (for the night benchmark)

19 years agofreshNamesGenerator moved into cic_proof_checking.
Andrea Asperti [Tue, 19 Jul 2005 11:17:13 +0000 (11:17 +0000)]
freshNamesGenerator moved into cic_proof_checking.

19 years agoMoved freshNameGenerator inside cic_proof_checking (and revised).
Andrea Asperti [Tue, 19 Jul 2005 11:13:33 +0000 (11:13 +0000)]
Moved freshNameGenerator inside cic_proof_checking (and revised).
CVS :

19 years agoNew naming policy for local variables.
Andrea Asperti [Tue, 19 Jul 2005 11:11:52 +0000 (11:11 +0000)]
New naming policy for local variables.

19 years agodo_tests.sh now returns with an error if one of the compilations fail
Claudio Sacerdoti Coen [Tue, 19 Jul 2005 11:02:21 +0000 (11:02 +0000)]
do_tests.sh now returns with an error if one of the compilations fail

19 years agothe decompose tactic is now working
Ferruccio Guidi [Tue, 19 Jul 2005 10:26:24 +0000 (10:26 +0000)]
the decompose tactic is now working

19 years agoavoids generating a wrong/empty/dummy depend
Enrico Tassi [Tue, 19 Jul 2005 09:59:04 +0000 (09:59 +0000)]
avoids generating a wrong/empty/dummy depend

19 years agoBug fixed: matitaclean and matitadep now ignores every parsing errors and
Enrico Tassi [Tue, 19 Jul 2005 09:57:55 +0000 (09:57 +0000)]
Bug fixed: matitaclean and matitadep now ignores every parsing errors and
simply continues. Before it used to avoid cleaning things and --- much worst ---
generating an empty .depend.

19 years agohandled difference associativity for the same level of the extensible grammar
Stefano Zacchiroli [Tue, 19 Jul 2005 09:37:09 +0000 (09:37 +0000)]
handled difference associativity for the same level of the extensible grammar
(no more "<W> changing associativity of level ..." messages)

19 years ago- A few suggestions on how to solve a few bugs
Claudio Sacerdoti Coen [Mon, 18 Jul 2005 17:22:07 +0000 (17:22 +0000)]
- A few suggestions on how to solve a few bugs
- GUI bugs reordered to have the easiest first

19 years agoBug fixed: the "find" command now scrolls the window appropriately.
Claudio Sacerdoti Coen [Mon, 18 Jul 2005 16:58:38 +0000 (16:58 +0000)]
Bug fixed: the "find" command now scrolls the window appropriately.

19 years ago...
Claudio Sacerdoti Coen [Mon, 18 Jul 2005 16:58:20 +0000 (16:58 +0000)]
...