]>
matita.cs.unibo.it Git - helm.git/log
Andrea Asperti [Wed, 16 Jul 2003 14:12:02 +0000 (14:12 +0000)]
Several changes (the beginning of a new era???)
1. stuff related to transformations (stylesheets and so on)
moved from gTopLevel to the new library cic_transformations
2. porting of the stylesheets to old plain ocaml code by Andrea Asperti.
Also in cic_transformations.
Disclaimer:
A. the ocaml transformations are still incomplete and under development.
They are a bit more performant, though. (just a few order of magnitudes)
B. the cic_transformation library seems a bit of a mess right now.
Much clean-up needed.
pmasoudi [Wed, 16 Jul 2003 12:48:25 +0000 (12:48 +0000)]
added persit-file-implementation.
Luca Padovani [Wed, 16 Jul 2003 12:46:11 +0000 (12:46 +0000)]
* changed name to control factory
Luca Padovani [Wed, 16 Jul 2003 08:45:34 +0000 (08:45 +0000)]
* updated the help file to reflect the new syntax (reload/remove)
Luca Padovani [Wed, 16 Jul 2003 08:39:41 +0000 (08:39 +0000)]
* syntax update for "remove all stylesheets" in control.js
* reloadAll function created
Luca Padovani [Tue, 15 Jul 2003 17:45:16 +0000 (17:45 +0000)]
* added .pc file
* IDL interface version computed from package version
Claudio Sacerdoti Coen [Tue, 15 Jul 2003 16:02:25 +0000 (16:02 +0000)]
Camera ready.
Luca Padovani [Tue, 15 Jul 2003 15:06:30 +0000 (15:06 +0000)]
* substituting the right version variable
Luca Padovani [Tue, 15 Jul 2003 15:05:28 +0000 (15:05 +0000)]
* wrong variable for version
Luca Padovani [Tue, 15 Jul 2003 15:03:27 +0000 (15:03 +0000)]
* patched version of shared library
Luca Padovani [Tue, 15 Jul 2003 14:54:22 +0000 (14:54 +0000)]
* first snapshot
Stefano Zacchiroli [Tue, 15 Jul 2003 14:50:42 +0000 (14:50 +0000)]
merged CSC's typos squashing
Stefano Zacchiroli [Tue, 15 Jul 2003 10:14:24 +0000 (10:14 +0000)]
fixed "s" typos
Ferruccio Guidi [Tue, 15 Jul 2003 09:17:59 +0000 (09:17 +0000)]
description for "Irene Schena" added in authors.html
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
Stefano Zacchiroli [Tue, 15 Jul 2003 06:35:42 +0000 (06:35 +0000)]
bumped version to 0.0.5
Claudio Sacerdoti Coen [Mon, 14 Jul 2003 17:05:15 +0000 (17:05 +0000)]
Towards the camera ready.
Stefano Zacchiroli [Mon, 14 Jul 2003 09:19:54 +0000 (09:19 +0000)]
debian release 0.0.4-7
Stefano Zacchiroli [Sat, 12 Jul 2003 12:18:09 +0000 (12:18 +0000)]
debian release 0.4.3-3
Stefano Zacchiroli [Fri, 11 Jul 2003 13:29:58 +0000 (13:29 +0000)]
reordered link order
Claudio Sacerdoti Coen [Fri, 11 Jul 2003 10:05:10 +0000 (10:05 +0000)]
Version dumped.
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.
Ferruccio Guidi [Thu, 10 Jul 2003 14:38:34 +0000 (14:38 +0000)]
prose patched
Ferruccio Guidi [Thu, 10 Jul 2003 10:47:19 +0000 (10:47 +0000)]
links page added
Ferruccio Guidi [Wed, 9 Jul 2003 16:33:36 +0000 (16:33 +0000)]
implementation and whatsnew pages added
Ferruccio Guidi [Thu, 3 Jul 2003 14:14:49 +0000 (14:14 +0000)]
"backPointer" metadata enabled
Ferruccio Guidi [Thu, 3 Jul 2003 10:55:47 +0000 (10:55 +0000)]
new "light" implementation of intersection (compatible with the generator)
Ferruccio Guidi [Wed, 2 Jul 2003 17:34:09 +0000 (17:34 +0000)]
rendering of "meet" patched
Claudio Sacerdoti Coen [Wed, 2 Jul 2003 11:37:18 +0000 (11:37 +0000)]
Bug fixed: deselecting a constraint just forgot its depth.
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
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.