]>
matita.cs.unibo.it Git - helm.git/log
Wilmer Ricciotti [Wed, 20 Jul 2011 16:11:12 +0000 (16:11 +0000)]
Matitaweb: fixed a bug concerning matita/html/xml escaping, which showed when
retrieving some nasty scripts from the server.
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)
Ferruccio Guidi [Tue, 19 Jul 2011 20:39:43 +0000 (20:39 +0000)]
first main property of drop closed
Ferruccio Guidi [Tue, 19 Jul 2011 15:12:25 +0000 (15:12 +0000)]
- drop_main: bug fix
- pr_lift: closed!
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!
Ferruccio Guidi [Tue, 19 Jul 2011 10:36:20 +0000 (10:36 +0000)]
one main property 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 :-((
Ferruccio Guidi [Sun, 17 Jul 2011 18:33:56 +0000 (18:33 +0000)]
more lemmas and some generated logical constants for them
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 15:02:24 +0000 (15:02 +0000)]
The name of the constructor for jmeq changed.
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.
Claudio Sacerdoti Coen [Fri, 15 Jul 2011 14:41:20 +0000 (14:41 +0000)]
Use replace when switching tabs (see previous commit).
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))
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.
Wilmer Ricciotti [Thu, 14 Jul 2011 15:11:15 +0000 (15:11 +0000)]
Changes to TeX-macro conversion.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:57:04 +0000 (14:57 +0000)]
Matitaweb: Bugfix for TeX-macro conversion.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:51:33 +0000 (14:51 +0000)]
Matitaweb: changes to utf8MacroTable.js
Wilmer Ricciotti [Thu, 14 Jul 2011 14:47:58 +0000 (14:47 +0000)]
Matitaweb: changes to utf8MacroTable.js.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:41:22 +0000 (14:41 +0000)]
Matitaweb: TeX-like macro handling.
Wilmer Ricciotti [Thu, 14 Jul 2011 14:02:50 +0000 (14:02 +0000)]
Changes to utf8MacroTable.js.
Wilmer Ricciotti [Thu, 14 Jul 2011 13:58:23 +0000 (13:58 +0000)]
Added Utf8MacroTable for MatitaWeb.
Wilmer Ricciotti [Thu, 14 Jul 2011 12:43:13 +0000 (12:43 +0000)]
More keyboard handling tests
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
Wilmer Ricciotti [Wed, 13 Jul 2011 15:49:47 +0000 (15:49 +0000)]
more tests on keyboard handling.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:30:29 +0000 (15:30 +0000)]
more tests on keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:28:54 +0000 (15:28 +0000)]
more tests on keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:16:40 +0000 (15:16 +0000)]
more keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:08:07 +0000 (15:08 +0000)]
more keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:02:53 +0000 (15:02 +0000)]
more keyboard events tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 15:00:43 +0000 (15:00 +0000)]
more keyboard tests.
Wilmer Ricciotti [Wed, 13 Jul 2011 14:46:06 +0000 (14:46 +0000)]
more keyboard events tests
Wilmer Ricciotti [Wed, 13 Jul 2011 14:36:07 +0000 (14:36 +0000)]
more keyboard event tests
Wilmer Ricciotti [Wed, 13 Jul 2011 14:25:54 +0000 (14:25 +0000)]
more tests with keyboard events.
Wilmer Ricciotti [Wed, 13 Jul 2011 14:22:02 +0000 (14:22 +0000)]
minor bugfix
Wilmer Ricciotti [Wed, 13 Jul 2011 14:09:52 +0000 (14:09 +0000)]
Testing keyboard events handling.
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
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
Wilmer Ricciotti [Thu, 23 Jun 2011 14:09:15 +0000 (14:09 +0000)]
Added facility for resetting the library.
Wilmer Ricciotti [Thu, 23 Jun 2011 14:05:34 +0000 (14:05 +0000)]
...
Wilmer Ricciotti [Thu, 23 Jun 2011 14:03:05 +0000 (14:03 +0000)]
Added matitaweb administration panel.
Claudio Sacerdoti Coen [Wed, 22 Jun 2011 21:05:44 +0000 (21:05 +0000)]
Possible assert false case implemented
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).
Wilmer Ricciotti [Wed, 22 Jun 2011 15:23:55 +0000 (15:23 +0000)]
Fix to matitaweb library dialog box.
Wilmer Ricciotti [Wed, 22 Jun 2011 15:20:52 +0000 (15:20 +0000)]
Fixes to library dialog box in matitaweb.
Wilmer Ricciotti [Wed, 22 Jun 2011 14:59:38 +0000 (14:59 +0000)]
Opening scripts using the Library dialog (try 1).
Wilmer Ricciotti [Wed, 22 Jun 2011 13:41:05 +0000 (13:41 +0000)]
More changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:35:15 +0000 (13:35 +0000)]
More changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:31:14 +0000 (13:31 +0000)]
Changes to matitaweb.js (dialog box).
Wilmer Ricciotti [Wed, 22 Jun 2011 13:19:44 +0000 (13:19 +0000)]
Show library test 1.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:03:03 +0000 (13:03 +0000)]
More changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 13:01:55 +0000 (13:01 +0000)]
More changes to matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:59:43 +0000 (12:59 +0000)]
Fix in matitaweb.css.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:58:55 +0000 (12:58 +0000)]
Fix in matitaweb:index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:57:47 +0000 (12:57 +0000)]
Changes to matitaweb.css (dialog boxes).
Wilmer Ricciotti [Wed, 22 Jun 2011 12:56:37 +0000 (12:56 +0000)]
Changes to matitaweb.css (dialog boxes).
Wilmer Ricciotti [Wed, 22 Jun 2011 12:52:55 +0000 (12:52 +0000)]
More changes to matitaweb dialog boxes.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:39:51 +0000 (12:39 +0000)]
Second attempt at dialog boxes in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:28:03 +0000 (12:28 +0000)]
Bugfix in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:25:51 +0000 (12:25 +0000)]
First attempt at dialog boxes.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:40:54 +0000 (09:40 +0000)]
More bugfixes for matitaweb's viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:37:31 +0000 (09:37 +0000)]
Bugfix in matitaweb viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:33:23 +0000 (09:33 +0000)]
Matitaweb viewlib, part II.
Claudio Sacerdoti Coen [Wed, 22 Jun 2011 09:32:36 +0000 (09:32 +0000)]
Escaping exceptions are now captured.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:06:32 +0000 (09:06 +0000)]
Added viewlib to matitaweb.
Ferruccio Guidi [Tue, 21 Jun 2011 20:35:04 +0000 (20:35 +0000)]
missing ; to delimit syntax :(
Wilmer Ricciotti [Tue, 21 Jun 2011 15:31:11 +0000 (15:31 +0000)]
More bugfixes in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:19:53 +0000 (15:19 +0000)]
Bugfix in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:06:43 +0000 (15:06 +0000)]
Changed user library dir to users/
Wilmer Ricciotti [Tue, 21 Jun 2011 14:58:49 +0000 (14:58 +0000)]
Added generation of HTML representation of the library.
Andrea Asperti [Tue, 21 Jun 2011 13:56:49 +0000 (13:56 +0000)]
Some progress
Andrea Asperti [Mon, 20 Jun 2011 09:16:00 +0000 (09:16 +0000)]
ported reduction.ma
Andrea Asperti [Mon, 20 Jun 2011 08:31:54 +0000 (08:31 +0000)]
Ported par_reduction
Andrea Asperti [Mon, 20 Jun 2011 07:38:34 +0000 (07:38 +0000)]
ported substs and subterms
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
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 11:32:30 +0000 (11:32 +0000)]
Unprotected List.fold_left2.
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)]
Remove the daemon :-)
Andrea Asperti [Fri, 17 Jun 2011 09:49:27 +0000 (09:49 +0000)]
New syntax of dummy with the type
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
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.
Wilmer Ricciotti [Thu, 16 Jun 2011 14:00:17 +0000 (14:00 +0000)]
Added location of the weblib repository to matita.conf.xml.in.
Wilmer Ricciotti [Thu, 16 Jun 2011 13:53:23 +0000 (13:53 +0000)]
Added repository for the shared library to be used by matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 16:15:09 +0000 (16:15 +0000)]
(Almost) working multi-user matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 14:13:24 +0000 (14:13 +0000)]
Logout (partial work) (multi-user matita)
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.
Ferruccio Guidi [Tue, 14 Jun 2011 19:00:26 +0000 (19:00 +0000)]
some restructuring
Ferruccio Guidi [Tue, 14 Jun 2011 18:24:05 +0000 (18:24 +0000)]
more lemmas to prove and a correction in subst
Ferruccio Guidi [Mon, 13 Jun 2011 17:59:58 +0000 (17:59 +0000)]
more notation and one more lemma to prove :(
Ferruccio Guidi [Mon, 13 Jun 2011 13:12:10 +0000 (13:12 +0000)]
reductions rules and one lemma
Ferruccio Guidi [Sun, 12 Jun 2011 17:25:50 +0000 (17:25 +0000)]
more properties of relocation
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.
Wilmer Ricciotti [Thu, 9 Jun 2011 15:27:04 +0000 (15:27 +0000)]
Fixes bugs in the Matitaweb UI.
Wilmer Ricciotti [Wed, 8 Jun 2011 15:55:47 +0000 (15:55 +0000)]
Fix for internet explorer (but still works badly).
Wilmer Ricciotti [Wed, 8 Jun 2011 15:52:31 +0000 (15:52 +0000)]
Cosmetic changes.
Wilmer Ricciotti [Wed, 8 Jun 2011 12:04:28 +0000 (12:04 +0000)]
Fixed a bug in the retract command of Matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:22:14 +0000 (11:22 +0000)]
Logo for use in matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:14:02 +0000 (11:14 +0000)]
Removed dependency of Matitaweb from GTK libraries.
Ferruccio Guidi [Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)]
- we removed the reduction-related item categorization
- some renaming
Wilmer Ricciotti [Tue, 7 Jun 2011 15:12:00 +0000 (15:12 +0000)]
Removed hardcoded include paths from matitadaemon.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:54 +0000 (14:52 +0000)]
Some changes in the Makefile for matitaweb.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:30 +0000 (14:52 +0000)]
Fixes record projections (see matita 1.0 branch)
Wilmer Ricciotti [Tue, 7 Jun 2011 14:36:36 +0000 (14:36 +0000)]
Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd