]>
matita.cs.unibo.it Git - helm.git/log
no author [Tue, 16 Dec 2003 17:00:48 +0000 (17:00 +0000)]
This commit was manufactured by cvs2svn to create tag 'V_0_2_2'.
Stefano Zacchiroli [Tue, 16 Dec 2003 17:00:48 +0000 (17:00 +0000)]
removed dependency on netclient, use http_client module from ocaml-http
Stefano Zacchiroli [Tue, 16 Dec 2003 16:49:38 +0000 (16:49 +0000)]
added parse_response_fst_line
Stefano Zacchiroli [Tue, 16 Dec 2003 16:49:04 +0000 (16:49 +0000)]
- return (or iter on) just http response's body
- s/http_get_iter_buf/http_get_iter/
- commented interface files
Stefano Zacchiroli [Tue, 16 Dec 2003 16:48:02 +0000 (16:48 +0000)]
added Malformed_response exception
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:52 +0000 (16:17 +0000)]
added http_client module
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:40 +0000 (16:17 +0000)]
rebuilt
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:23 +0000 (16:17 +0000)]
ported to ocaml 3.07
Stefano Zacchiroli [Tue, 16 Dec 2003 16:06:35 +0000 (16:06 +0000)]
renamed META*.src to meta*.src so that ocamlfind list doesn't list both
src and real METAs
Stefano Zacchiroli [Tue, 16 Dec 2003 15:59:54 +0000 (15:59 +0000)]
- fixed logging in log window so that spurious html tags are no longer
printed
- factorized a lot of error handling code in invokeTactics
- moved (and reimplemented) logger class to ui_logger module
Stefano Zacchiroli [Tue, 16 Dec 2003 15:58:38 +0000 (15:58 +0000)]
renamed module "logger" to "cicLogger" to avoid confusion with user
interface logger
Stefano Zacchiroli [Tue, 16 Dec 2003 13:50:41 +0000 (13:50 +0000)]
sample script.sh which read META files from ocaml/METAS
Stefano Zacchiroli [Tue, 16 Dec 2003 13:49:09 +0000 (13:49 +0000)]
moved META files in METAS/ dir
Stefano Zacchiroli [Tue, 16 Dec 2003 08:55:00 +0000 (08:55 +0000)]
added support for cic_textual_parser2 module
Stefano Zacchiroli [Mon, 15 Dec 2003 23:00:39 +0000 (23:00 +0000)]
new experimental cic textual parser: checkin
Stefano Zacchiroli [Wed, 10 Dec 2003 16:57:54 +0000 (16:57 +0000)]
close RC bug regarding rebuilding with newer gthmathview
Ferruccio Guidi [Mon, 8 Dec 2003 16:22:24 +0000 (16:22 +0000)]
mathql documentation for version 4
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:39 +0000 (16:58 +0000)]
debian version 0.0.4-3
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:06 +0000 (16:58 +0000)]
added -thread option where needed to make new findlib happy
Stefano Zacchiroli [Thu, 4 Dec 2003 16:57:50 +0000 (16:57 +0000)]
ignore environments
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:48 +0000 (14:47 +0000)]
esplicitely add -thread parameter to all compiler invocations
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:28 +0000 (14:47 +0000)]
use a list of getter maps
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:03 +0000 (14:47 +0000)]
rebuilt
Ferruccio Guidi [Tue, 2 Dec 2003 17:11:10 +0000 (17:11 +0000)]
sort CProp added
Claudio Sacerdoti Coen [Thu, 20 Nov 2003 11:30:01 +0000 (11:30 +0000)]
The tmp is now cleared from the http___* files.
Ferruccio Guidi [Thu, 13 Nov 2003 11:37:31 +0000 (11:37 +0000)]
updated
Luca Padovani [Fri, 7 Nov 2003 12:59:46 +0000 (12:59 +0000)]
* debugging messages and dumpes commented out
Claudio Sacerdoti Coen [Fri, 7 Nov 2003 11:04:17 +0000 (11:04 +0000)]
Porting to lablgtk2 completed.
Claudio Sacerdoti Coen [Fri, 7 Nov 2003 09:34:02 +0000 (09:34 +0000)]
The hbugs client interface is almost working again.
Claudio Sacerdoti Coen [Thu, 6 Nov 2003 16:58:54 +0000 (16:58 +0000)]
HBugs compile again (but it does not do anything right now: still to be
ported correctly to lablgtk2)
Claudio Sacerdoti Coen [Thu, 6 Nov 2003 16:56:53 +0000 (16:56 +0000)]
First release that compiles under lablgtk2 (but it does not work, actually!)
Ferruccio Guidi [Wed, 5 Nov 2003 17:33:55 +0000 (17:33 +0000)]
updated to version 4
Ferruccio Guidi [Wed, 5 Nov 2003 10:04:44 +0000 (10:04 +0000)]
updated to version 1.4
Luca Padovani [Tue, 4 Nov 2003 10:49:02 +0000 (10:49 +0000)]
* first upgrade to the new error logging mechanism
Claudio Sacerdoti Coen [Mon, 3 Nov 2003 12:26:51 +0000 (12:26 +0000)]
*** empty log message ***
Ferruccio Guidi [Wed, 29 Oct 2003 15:40:25 +0000 (15:40 +0000)]
some interfaces changed to prepare the mathql code for version 1.4
Luca Padovani [Wed, 29 Oct 2003 10:25:32 +0000 (10:25 +0000)]
* removed dependency from liblablgtk-ocaml{,-dev}
Luca Padovani [Wed, 29 Oct 2003 10:25:04 +0000 (10:25 +0000)]
* added profiling options
Luca Padovani [Wed, 29 Oct 2003 10:01:20 +0000 (10:01 +0000)]
* temporarily removed hbugs dependency
Luca Padovani [Wed, 29 Oct 2003 10:00:57 +0000 (10:00 +0000)]
* updated for gtk2
* temporarily removed hbugs
* temporarily removed html widget using a plain text widget instead
Luca Padovani [Wed, 29 Oct 2003 09:59:56 +0000 (09:59 +0000)]
* updated for gtk2
Stefano Zacchiroli [Wed, 29 Oct 2003 09:38:22 +0000 (09:38 +0000)]
debian version 0.0.4-2
Luca Padovani [Wed, 29 Oct 2003 09:38:09 +0000 (09:38 +0000)]
* this implements the new instantiation for gtkmathview
Luca Padovani [Wed, 29 Oct 2003 09:18:47 +0000 (09:18 +0000)]
* GEdit -> GText
Luca Padovani [Wed, 29 Oct 2003 09:17:30 +0000 (09:17 +0000)]
* variant types changed for selection mode
Luca Padovani [Tue, 21 Oct 2003 12:50:37 +0000 (12:50 +0000)]
* fixed O_S variable for ocamlmklib on hppa arch
Stefano Zacchiroli [Tue, 21 Oct 2003 12:49:30 +0000 (12:49 +0000)]
- debian release 0.0.6-3
- use .o objects from .libs directory so that they are PIC
(fix build failure on hppa)
Luca Padovani [Tue, 21 Oct 2003 08:28:42 +0000 (08:28 +0000)]
* first version of the profile manager committed
Luca Padovani [Sat, 18 Oct 2003 10:42:07 +0000 (10:42 +0000)]
* added timer for profiling the editor
Luca Padovani [Fri, 17 Oct 2003 14:01:18 +0000 (14:01 +0000)]
* added daemon
* fixed minor bugs
Luca Padovani [Fri, 17 Oct 2003 09:53:46 +0000 (09:53 +0000)]
* oo interface
Luca Padovani [Fri, 17 Oct 2003 09:38:12 +0000 (09:38 +0000)]
* first files added to cvs
Stefano Zacchiroli [Mon, 13 Oct 2003 07:29:07 +0000 (07:29 +0000)]
debian version 0.5.1-2
Stefano Zacchiroli [Mon, 13 Oct 2003 07:14:47 +0000 (07:14 +0000)]
debian version 0.5.1-1
Stefano Zacchiroli [Fri, 10 Oct 2003 07:55:13 +0000 (07:55 +0000)]
debian snapshot version 0.0.6-2
Luca Padovani [Wed, 8 Oct 2003 06:13:50 +0000 (06:13 +0000)]
* snapshot for gtk2
Luca Padovani [Tue, 7 Oct 2003 17:24:38 +0000 (17:24 +0000)]
* added new .ml files to be ignored
Luca Padovani [Tue, 7 Oct 2003 17:20:14 +0000 (17:20 +0000)]
* lablgtk -> lablgtk2
Luca Padovani [Tue, 7 Oct 2003 17:18:43 +0000 (17:18 +0000)]
* removed debugging Printfs'
Luca Padovani [Tue, 7 Oct 2003 10:40:32 +0000 (10:40 +0000)]
* removed currified constructors everywhere. A bug in the ocaml compiler
allowed to use them, but the bug is now fixed so they cannot be used
anymore. Sorry fellows, next time choose a better compiler ;-)
Ferruccio Guidi [Mon, 6 Oct 2003 17:25:23 +0000 (17:25 +0000)]
hxp: performes several tasks among which some metadata extraction
Luca Padovani [Mon, 6 Oct 2003 09:17:32 +0000 (09:17 +0000)]
* minor fix
Luca Padovani [Mon, 6 Oct 2003 09:05:16 +0000 (09:05 +0000)]
* removed spec file
* updated configuration
* added .props file for lablgtk2
Luca Padovani [Mon, 6 Oct 2003 09:01:48 +0000 (09:01 +0000)]
* upgrade to lablgtk2
Luca Padovani [Mon, 6 Oct 2003 08:58:47 +0000 (08:58 +0000)]
* checking for lablgtk2
Luca Padovani [Mon, 6 Oct 2003 08:46:46 +0000 (08:46 +0000)]
* update dependency: lablgtk -> lablgtk2
Luca Padovani [Sun, 5 Oct 2003 08:02:30 +0000 (08:02 +0000)]
* added popup menu, implemented some functions
Stefano Zacchiroli [Sat, 4 Oct 2003 13:29:11 +0000 (13:29 +0000)]
debian package for ocaml 3.07
Luca Padovani [Sat, 4 Oct 2003 08:21:57 +0000 (08:21 +0000)]
* changed version in configure.ac
* gdome_xslt.c renamed into x_gdome_xslt.c otherwise there was a conflict
with make rules that prevented gdome_xslt.o from being built correctly
Luca Padovani [Fri, 3 Oct 2003 14:14:51 +0000 (14:14 +0000)]
* further code cleanup
Luca Padovani [Fri, 3 Oct 2003 14:03:15 +0000 (14:03 +0000)]
* updated #include directives
* clean up of some makefiles
Andrea Asperti [Wed, 1 Oct 2003 13:08:08 +0000 (13:08 +0000)]
* the main function MUST return 0 to communicate everything was OK
Andrea Asperti [Wed, 1 Oct 2003 08:39:17 +0000 (08:39 +0000)]
* new version of metadata extraction
* metadata are inserted directly without creating the RDF document
Luca Padovani [Fri, 26 Sep 2003 15:55:54 +0000 (15:55 +0000)]
* the regular expressions must have $ otherwise the shortest match
will be found first and the annotations will never show up
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:41:25 +0000 (17:41 +0000)]
...
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:40:08 +0000 (17:40 +0000)]
Reindentation.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:39:01 +0000 (17:39 +0000)]
ProofEngine.goal := ==> set_proof_engine_goal
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:33:30 +0000 (17:33 +0000)]
Reindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:25:28 +0000 (17:25 +0000)]
ProofEngine.proof is now an abstract data type (since we plan to have OMDoc
in the future as the persistent format).
Ferruccio Guidi [Tue, 23 Sep 2003 17:06:50 +0000 (17:06 +0000)]
patch
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 16:10:16 +0000 (16:10 +0000)]
This version of xmlDiff is much much much smarter than the previous one:
with the forthcoming version of gdome the performances will be doubled.
[ Unfortunately, it is still deadly slow. ]
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:58:28 +0000 (15:58 +0000)]
Reindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:56:42 +0000 (15:56 +0000)]
BU_Conversion + omit-conclusion is a mess. I have partially fixed the
problem by ignoring the omit-conclusion flag.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:55:28 +0000 (15:55 +0000)]
Debugging stuff removed.
Ferruccio Guidi [Tue, 23 Sep 2003 15:12:46 +0000 (15:12 +0000)]
Now mathql_generator compiles before mathql_interpreter.
This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 12:06:54 +0000 (12:06 +0000)]
Preliminary support for proof-tree enhanced: proof-trees are now shown
as views over .con files.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 11:12:38 +0000 (11:12 +0000)]
- added support for proof trees
- fixed typo in body.ann regexp
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 13:00:28 +0000 (13:00 +0000)]
clean_cache method added
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:57:01 +0000 (12:57 +0000)]
cleancache ==> clean_cache
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:44:51 +0000 (12:44 +0000)]
Clean cache method added.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 11:58:43 +0000 (11:58 +0000)]
param.framewidth = 150 (hard-coded ;-( pour Hanane ;-((((((((((
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 11:33:47 +0000 (11:33 +0000)]
Following an hyperlink from a proof-tree rendering now brings you to
the lambda-term rendering of the proof statement.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 08:10:14 +0000 (08:10 +0000)]
Preliminary commit to support Hanane's proof-tree rendering.
Claudio Sacerdoti Coen [Thu, 18 Sep 2003 15:41:11 +0000 (15:41 +0000)]
prop.media-type and prop.encoding were _NOT_ considered when the
corresponding HTML <meta/> was generated. Fixed.
Claudio Sacerdoti Coen [Wed, 17 Sep 2003 12:27:50 +0000 (12:27 +0000)]
www-sop.inria.fr
^
Hyphen in the name of the server were not allowed. Fixed.
Stefano Zacchiroli [Sun, 14 Sep 2003 00:03:18 +0000 (00:03 +0000)]
- bumped copyright years
- added support for proof checker environment dump/save/restore
- added support for hbugs notify upon goal change (disabled by default)
- added (re)submit option to hbugs menu
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:34 +0000 (00:01 +0000)]
- converted TAB to spaces
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:25 +0000 (00:01 +0000)]
- clear hints list upon status submit
- converted TAB to spaces
Stefano Zacchiroli [Sat, 13 Sep 2003 23:59:22 +0000 (23:59 +0000)]
- added support for dumping environment to file on exit (disabled by default)
- added environment restore on boot
Stefano Zacchiroli [Sat, 13 Sep 2003 23:58:39 +0000 (23:58 +0000)]
added environment setting (set by fill_template)