]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years ago1) Matitaweb now disambiguates scripts as it runs them
Wilmer Ricciotti [Wed, 20 Jul 2011 15:34:52 +0000 (15:34 +0000)]
1) Matitaweb now disambiguates scripts as it runs them

2) Fixed bugs in HTML escaping (also changed the syntax of annotations in
   matita scripts)

12 years agofirst main property of drop closed
Ferruccio Guidi [Tue, 19 Jul 2011 20:39:43 +0000 (20:39 +0000)]
first main property of drop closed

12 years ago- drop_main: bug fix
Ferruccio Guidi [Tue, 19 Jul 2011 15:12:25 +0000 (15:12 +0000)]
- drop_main: bug fix
- pr_lift: closed!

12 years ago- nnAuto.ml: width overflows are warnings, not errors
Ferruccio Guidi [Tue, 19 Jul 2011 14:25:24 +0000 (14:25 +0000)]
- nnAuto.ml: width overflows are warnings, not errors
- matitaScript.ml: backup source file with ~ reactivated
- lambda-delta: main properies of lift closed!

12 years agoone main property of lift closed
Ferruccio Guidi [Tue, 19 Jul 2011 10:36:20 +0000 (10:36 +0000)]
one main property of lift closed

12 years ago- functional properties of lift closed!
Ferruccio Guidi [Mon, 18 Jul 2011 19:17:42 +0000 (19:17 +0000)]
- functional properties of lift closed!
- the proof of a main property of lift was lost due to a segmentation
fault of auto :-((

12 years agomore lemmas and some generated logical constants for them
Ferruccio Guidi [Sun, 17 Jul 2011 18:33:56 +0000 (18:33 +0000)]
more lemmas and some generated logical constants for them

12 years agoThe name of the constructor for jmeq changed.
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 15:02:24 +0000 (15:02 +0000)]
The name of the constructor for jmeq changed.

12 years agoBug fixed: when we try to add an object and it is not _directly_ well typed
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 15:00:40 +0000 (15:00 +0000)]
Bug fixed: when we try to add an object and it is not _directly_ well typed
(i.e. it is not well typed, and not because it depends on a non-well-typed
object in the library), we should not remember it, since the user can change
the definition and try again.

12 years agoUse replace when switching tabs (see previous commit).
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 14:41:20 +0000 (14:41 +0000)]
Use replace when switching tabs (see previous commit).

12 years agoNew function replace to be used in place of time_travel every time the user
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 14:40:34 +0000 (14:40 +0000)]
New function replace to be used in place of time_travel every time the user
switches to a new tab. In this way, every tab is independent and it only sees
the objects defined in that tab. This fixes the following bug: in tab A go
down; go down in tab B; go up in tab A (at this point also the objects declared
in B where removed); do something in B or go up in B (BOOM))

12 years agoDead code removed from the interface. It is used internally via references.
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 14:30:49 +0000 (14:30 +0000)]
Dead code removed from the interface. It is used internally via references.

12 years agoChanges to TeX-macro conversion.
Wilmer Ricciotti [Thu, 14 Jul 2011 15:11:15 +0000 (15:11 +0000)]
Changes to TeX-macro conversion.

12 years agoMatitaweb: Bugfix for TeX-macro conversion.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:57:04 +0000 (14:57 +0000)]
Matitaweb: Bugfix for TeX-macro conversion.

12 years agoMatitaweb: changes to utf8MacroTable.js
Wilmer Ricciotti [Thu, 14 Jul 2011 14:51:33 +0000 (14:51 +0000)]
Matitaweb: changes to utf8MacroTable.js

12 years agoMatitaweb: changes to utf8MacroTable.js.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:47:58 +0000 (14:47 +0000)]
Matitaweb: changes to utf8MacroTable.js.

12 years agoMatitaweb: TeX-like macro handling.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:41:22 +0000 (14:41 +0000)]
Matitaweb: TeX-like macro handling.

12 years agoChanges to utf8MacroTable.js.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:02:50 +0000 (14:02 +0000)]
Changes to utf8MacroTable.js.

12 years agoAdded Utf8MacroTable for MatitaWeb.
Wilmer Ricciotti [Thu, 14 Jul 2011 13:58:23 +0000 (13:58 +0000)]
Added Utf8MacroTable for MatitaWeb.

12 years agoMore keyboard handling tests
Wilmer Ricciotti [Thu, 14 Jul 2011 12:43:13 +0000 (12:43 +0000)]
More keyboard handling tests

12 years ago- new definition of subst based on drop
Ferruccio Guidi [Wed, 13 Jul 2011 19:54:24 +0000 (19:54 +0000)]
- new definition of subst based on drop
- pr is now based on drop

12 years agomore tests on keyboard handling.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:49:47 +0000 (15:49 +0000)]
more tests on keyboard handling.

12 years agomore tests on keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:30:29 +0000 (15:30 +0000)]
more tests on keyboard events.

12 years agomore tests on keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:28:54 +0000 (15:28 +0000)]
more tests on keyboard events.

12 years agomore keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:16:40 +0000 (15:16 +0000)]
more keyboard events tests.

12 years agomore keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:08:07 +0000 (15:08 +0000)]
more keyboard events tests.

12 years agomore keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:02:53 +0000 (15:02 +0000)]
more keyboard events tests.

12 years agomore keyboard tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:00:43 +0000 (15:00 +0000)]
more keyboard tests.

12 years agomore keyboard events tests
Wilmer Ricciotti [Wed, 13 Jul 2011 14:46:06 +0000 (14:46 +0000)]
more keyboard events tests

12 years agomore keyboard event tests
Wilmer Ricciotti [Wed, 13 Jul 2011 14:36:07 +0000 (14:36 +0000)]
more keyboard event tests

12 years agomore tests with keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 14:25:54 +0000 (14:25 +0000)]
more tests with keyboard events.

12 years agominor bugfix
Wilmer Ricciotti [Wed, 13 Jul 2011 14:22:02 +0000 (14:22 +0000)]
minor bugfix

12 years agoTesting keyboard events handling.
Wilmer Ricciotti [Wed, 13 Jul 2011 14:09:52 +0000 (14:09 +0000)]
Testing keyboard events handling.

12 years agolong file names caused indentation underflow (String.make) when times
Ferruccio Guidi [Sat, 25 Jun 2011 19:26:02 +0000 (19:26 +0000)]
long file names caused indentation underflow (String.make) when times
were displayed

12 years ago- some depend files
Ferruccio Guidi [Sat, 25 Jun 2011 15:49:51 +0000 (15:49 +0000)]
- some depend files
- bug fix in grafiteAstPp.ml
- some assertions in matitaEngine.ml

12 years agoAdded facility for resetting the library.
Wilmer Ricciotti [Thu, 23 Jun 2011 14:09:15 +0000 (14:09 +0000)]
Added facility for resetting the library.

12 years ago...
Wilmer Ricciotti [Thu, 23 Jun 2011 14:05:34 +0000 (14:05 +0000)]
...

12 years agoAdded matitaweb administration panel.
Wilmer Ricciotti [Thu, 23 Jun 2011 14:03:05 +0000 (14:03 +0000)]
Added matitaweb administration panel.

12 years agoPossible assert false case implemented
Claudio Sacerdoti Coen [Wed, 22 Jun 2011 21:05:44 +0000 (21:05 +0000)]
Possible assert false case implemented

12 years agoRemoved filename input box from index.html (just browse the library now).
Wilmer Ricciotti [Wed, 22 Jun 2011 15:32:03 +0000 (15:32 +0000)]
Removed filename input box from index.html (just browse the library now).

12 years agoFix to matitaweb library dialog box.
Wilmer Ricciotti [Wed, 22 Jun 2011 15:23:55 +0000 (15:23 +0000)]
Fix to matitaweb library dialog box.

12 years agoFixes to library dialog box in matitaweb.
Wilmer Ricciotti [Wed, 22 Jun 2011 15:20:52 +0000 (15:20 +0000)]
Fixes to library dialog box in matitaweb.

12 years agoOpening scripts using the Library dialog (try 1).
Wilmer Ricciotti [Wed, 22 Jun 2011 14:59:38 +0000 (14:59 +0000)]
Opening scripts using the Library dialog (try 1).

12 years agoMore changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:41:05 +0000 (13:41 +0000)]
More changes to matitaweb.css.

12 years agoMore changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:35:15 +0000 (13:35 +0000)]
More changes to matitaweb.css.

12 years agoChanges to matitaweb.js (dialog box).
Wilmer Ricciotti [Wed, 22 Jun 2011 13:31:14 +0000 (13:31 +0000)]
Changes to matitaweb.js (dialog box).

12 years agoShow library test 1.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:19:44 +0000 (13:19 +0000)]
Show library test 1.

12 years agoMore changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:03:03 +0000 (13:03 +0000)]
More changes to matitaweb.css.

12 years agoMore changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:01:55 +0000 (13:01 +0000)]
More changes to matitaweb.css.

12 years agoFix in matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:59:43 +0000 (12:59 +0000)]
Fix in matitaweb.css.

12 years agoFix in matitaweb:index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:58:55 +0000 (12:58 +0000)]
Fix in matitaweb:index.html.

12 years agoChanges to matitaweb.css (dialog boxes).
Wilmer Ricciotti [Wed, 22 Jun 2011 12:57:47 +0000 (12:57 +0000)]
Changes to matitaweb.css (dialog boxes).

12 years agoChanges to matitaweb.css (dialog boxes).
Wilmer Ricciotti [Wed, 22 Jun 2011 12:56:37 +0000 (12:56 +0000)]
Changes to matitaweb.css (dialog boxes).

12 years agoMore changes to matitaweb dialog boxes.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:52:55 +0000 (12:52 +0000)]
More changes to matitaweb dialog boxes.

12 years agoSecond attempt at dialog boxes in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:39:51 +0000 (12:39 +0000)]
Second attempt at dialog boxes in index.html.

12 years agoBugfix in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:28:03 +0000 (12:28 +0000)]
Bugfix in index.html.

12 years agoFirst attempt at dialog boxes.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:25:51 +0000 (12:25 +0000)]
First attempt at dialog boxes.

12 years agoMore bugfixes for matitaweb's viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:40:54 +0000 (09:40 +0000)]
More bugfixes for matitaweb's viewlib.

12 years agoBugfix in matitaweb viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:37:31 +0000 (09:37 +0000)]
Bugfix in matitaweb viewlib.

12 years agoMatitaweb viewlib, part II.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:33:23 +0000 (09:33 +0000)]
Matitaweb viewlib, part II.

12 years agoEscaping exceptions are now captured.
Claudio Sacerdoti Coen [Wed, 22 Jun 2011 09:32:36 +0000 (09:32 +0000)]
Escaping exceptions are now captured.

12 years agoAdded viewlib to matitaweb.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:06:32 +0000 (09:06 +0000)]
Added viewlib to matitaweb.

12 years agomissing ; to delimit syntax :(
Ferruccio Guidi [Tue, 21 Jun 2011 20:35:04 +0000 (20:35 +0000)]
missing ; to delimit syntax :(

12 years agoMore bugfixes in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:31:11 +0000 (15:31 +0000)]
More bugfixes in matitaFilesystem.ml

12 years agoBugfix in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:19:53 +0000 (15:19 +0000)]
Bugfix in matitaFilesystem.ml

12 years agoChanged user library dir to users/
Wilmer Ricciotti [Tue, 21 Jun 2011 15:06:43 +0000 (15:06 +0000)]
Changed user library dir to users/

12 years agoAdded generation of HTML representation of the library.
Wilmer Ricciotti [Tue, 21 Jun 2011 14:58:49 +0000 (14:58 +0000)]
Added generation of HTML representation of the library.

12 years agoSome progress
Andrea Asperti [Tue, 21 Jun 2011 13:56:49 +0000 (13:56 +0000)]
Some progress

12 years agoported reduction.ma
Andrea Asperti [Mon, 20 Jun 2011 09:16:00 +0000 (09:16 +0000)]
ported reduction.ma

12 years agoPorted par_reduction
Andrea Asperti [Mon, 20 Jun 2011 08:31:54 +0000 (08:31 +0000)]
Ported par_reduction

12 years agoported substs and subterms
Andrea Asperti [Mon, 20 Jun 2011 07:38:34 +0000 (07:38 +0000)]
ported substs and subterms

12 years ago- xoa: more existential types
Ferruccio Guidi [Sat, 18 Jun 2011 14:29:50 +0000 (14:29 +0000)]
- xoa: more existential types
- ground: more arithmetics
- lift: more nasic inversion lemmas and some renaming

12 years agoUnprotected List.fold_left2.
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 11:32:30 +0000 (11:32 +0000)]
Unprotected List.fold_left2.

12 years agoRemove the daemon :-)
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)]
Remove the daemon :-)

12 years agoNew syntax of dummy with the type
Andrea Asperti [Fri, 17 Jun 2011 09:49:27 +0000 (09:49 +0000)]
New syntax of dummy with the type

12 years agoAdded a copy of lambdaN to extend the syntax of dummies with types
Andrea Asperti [Fri, 17 Jun 2011 09:01:29 +0000 (09:01 +0000)]
Added a copy of lambdaN to extend the syntax of dummies with types

12 years agoAdded module MatitaFilesystem, to be used for the management of the library
Wilmer Ricciotti [Thu, 16 Jun 2011 14:52:19 +0000 (14:52 +0000)]
Added module MatitaFilesystem, to be used for the management of the library
in matitaweb.

12 years agoAdded location of the weblib repository to matita.conf.xml.in.
Wilmer Ricciotti [Thu, 16 Jun 2011 14:00:17 +0000 (14:00 +0000)]
Added location of the weblib repository to matita.conf.xml.in.

12 years agoAdded repository for the shared library to be used by matitaweb.
Wilmer Ricciotti [Thu, 16 Jun 2011 13:53:23 +0000 (13:53 +0000)]
Added repository for the shared library to be used by matitaweb.

12 years ago(Almost) working multi-user matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 16:15:09 +0000 (16:15 +0000)]
(Almost) working multi-user matitaweb.

12 years agoLogout (partial work) (multi-user matita)
Wilmer Ricciotti [Wed, 15 Jun 2011 14:13:24 +0000 (14:13 +0000)]
Logout (partial work) (multi-user matita)

12 years agoMulti-user Matita (and Matitaweb): added user authentication (currently only
Wilmer Ricciotti [Wed, 15 Jun 2011 12:49:01 +0000 (12:49 +0000)]
Multi-user Matita (and Matitaweb): added user authentication (currently only
tested on hard-coded accounts). Proof-objects are saved in a user-specific
directory.

12 years agosome restructuring
Ferruccio Guidi [Tue, 14 Jun 2011 19:00:26 +0000 (19:00 +0000)]
some restructuring

12 years agomore lemmas to prove and a correction in subst
Ferruccio Guidi [Tue, 14 Jun 2011 18:24:05 +0000 (18:24 +0000)]
more lemmas to prove and a correction in subst

12 years agomore notation and one more lemma to prove :(
Ferruccio Guidi [Mon, 13 Jun 2011 17:59:58 +0000 (17:59 +0000)]
more notation and one more lemma to prove :(

12 years agoreductions rules and one lemma
Ferruccio Guidi [Mon, 13 Jun 2011 13:12:10 +0000 (13:12 +0000)]
reductions rules and one lemma

12 years agomore properties of relocation
Ferruccio Guidi [Sun, 12 Jun 2011 17:25:50 +0000 (17:25 +0000)]
more properties of relocation

12 years agoMulti-user matita: changed the status object to include a ``user'' method
Wilmer Ricciotti [Fri, 10 Jun 2011 12:56:04 +0000 (12:56 +0000)]
Multi-user matita: changed the status object to include a ``user'' method
containing an optional string, used to identify associated user.

12 years agoFixes bugs in the Matitaweb UI.
Wilmer Ricciotti [Thu, 9 Jun 2011 15:27:04 +0000 (15:27 +0000)]
Fixes bugs in the  Matitaweb UI.

12 years agoFix for internet explorer (but still works badly).
Wilmer Ricciotti [Wed, 8 Jun 2011 15:55:47 +0000 (15:55 +0000)]
Fix for internet explorer (but still works badly).

12 years agoCosmetic changes.
Wilmer Ricciotti [Wed, 8 Jun 2011 15:52:31 +0000 (15:52 +0000)]
Cosmetic changes.

12 years agoFixed a bug in the retract command of Matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 12:04:28 +0000 (12:04 +0000)]
Fixed a bug in the retract command of Matitaweb.

12 years agoLogo for use in matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:22:14 +0000 (11:22 +0000)]
Logo for use in matitaweb.

12 years agoRemoved dependency of Matitaweb from GTK libraries.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:14:02 +0000 (11:14 +0000)]
Removed dependency of Matitaweb from GTK libraries.

12 years ago- we removed the reduction-related item categorization
Ferruccio Guidi [Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)]
- we removed the reduction-related item categorization
- some renaming

12 years agoRemoved hardcoded include paths from matitadaemon.
Wilmer Ricciotti [Tue, 7 Jun 2011 15:12:00 +0000 (15:12 +0000)]
Removed hardcoded include paths from matitadaemon.

12 years agoSome changes in the Makefile for matitaweb.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:54 +0000 (14:52 +0000)]
Some changes in the Makefile for matitaweb.

12 years agoFixes record projections (see matita 1.0 branch)
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:30 +0000 (14:52 +0000)]
Fixes record projections (see matita 1.0 branch)

12 years agoMatitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd
Wilmer Ricciotti [Tue, 7 Jun 2011 14:36:36 +0000 (14:36 +0000)]
Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd

12 years agoThis can happen: when you use nodelta.
Claudio Sacerdoti Coen [Tue, 7 Jun 2011 12:13:27 +0000 (12:13 +0000)]
This can happen: when you use nodelta.