]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agoThis commit was manufactured by cvs2svn to create tag 'V_0_0_8'. V_0_0_8
no author [Tue, 16 Dec 2003 17:01:28 +0000 (17:01 +0000)]
This commit was manufactured by cvs2svn to create tag 'V_0_0_8'.

20 years agofixed typo in ocamldoc comment
Stefano Zacchiroli [Tue, 16 Dec 2003 17:01:28 +0000 (17:01 +0000)]
fixed typo in ocamldoc comment

20 years agoremoved dependency on netclient, use http_client module from ocaml-http
Stefano Zacchiroli [Tue, 16 Dec 2003 17:00:48 +0000 (17:00 +0000)]
removed dependency on netclient, use http_client module from ocaml-http

20 years agoadded parse_response_fst_line
Stefano Zacchiroli [Tue, 16 Dec 2003 16:49:38 +0000 (16:49 +0000)]
added parse_response_fst_line

20 years ago- return (or iter on) just http response's body
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

20 years agoadded Malformed_response exception
Stefano Zacchiroli [Tue, 16 Dec 2003 16:48:02 +0000 (16:48 +0000)]
added Malformed_response exception

20 years agoadded http_client module
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:52 +0000 (16:17 +0000)]
added http_client module

20 years agorebuilt
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:40 +0000 (16:17 +0000)]
rebuilt

20 years agoported to ocaml 3.07
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:23 +0000 (16:17 +0000)]
ported to ocaml 3.07

20 years agorenamed META*.src to meta*.src so that ocamlfind list doesn't list both
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

20 years ago- fixed logging in log window so that spurious html tags are no longer
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

20 years agorenamed module "logger" to "cicLogger" to avoid confusion with user
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

20 years agosample script.sh which read META files from ocaml/METAS
Stefano Zacchiroli [Tue, 16 Dec 2003 13:50:41 +0000 (13:50 +0000)]
sample script.sh which read META files from ocaml/METAS

20 years agomoved META files in METAS/ dir
Stefano Zacchiroli [Tue, 16 Dec 2003 13:49:09 +0000 (13:49 +0000)]
moved META files in METAS/ dir

20 years agoadded support for cic_textual_parser2 module
Stefano Zacchiroli [Tue, 16 Dec 2003 08:55:00 +0000 (08:55 +0000)]
added support for cic_textual_parser2 module

20 years agonew experimental cic textual parser: checkin
Stefano Zacchiroli [Mon, 15 Dec 2003 23:00:39 +0000 (23:00 +0000)]
new experimental cic textual parser: checkin

20 years agoclose RC bug regarding rebuilding with newer gthmathview
Stefano Zacchiroli [Wed, 10 Dec 2003 16:57:54 +0000 (16:57 +0000)]
close RC bug regarding rebuilding with newer gthmathview

20 years agomathql documentation for version 4
Ferruccio Guidi [Mon, 8 Dec 2003 16:22:24 +0000 (16:22 +0000)]
mathql documentation for version 4

20 years agodebian version 0.0.4-3
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:39 +0000 (16:58 +0000)]
debian version 0.0.4-3

20 years agoadded -thread option where needed to make new findlib happy
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:06 +0000 (16:58 +0000)]
added -thread option where needed to make new findlib happy

20 years agoignore environments
Stefano Zacchiroli [Thu, 4 Dec 2003 16:57:50 +0000 (16:57 +0000)]
ignore environments

20 years agoesplicitely add -thread parameter to all compiler invocations
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:48 +0000 (14:47 +0000)]
esplicitely add -thread parameter to all compiler invocations

20 years agouse a list of getter maps
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:28 +0000 (14:47 +0000)]
use a list of getter maps

20 years agorebuilt
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:03 +0000 (14:47 +0000)]
rebuilt

20 years agosort CProp added
Ferruccio Guidi [Tue, 2 Dec 2003 17:11:10 +0000 (17:11 +0000)]
sort CProp added

20 years agoThe tmp is now cleared from the http___* files.
Claudio Sacerdoti Coen [Thu, 20 Nov 2003 11:30:01 +0000 (11:30 +0000)]
The tmp is now cleared from the http___* files.

20 years agoupdated
Ferruccio Guidi [Thu, 13 Nov 2003 11:37:31 +0000 (11:37 +0000)]
updated

20 years ago* debugging messages and dumpes commented out
Luca Padovani [Fri, 7 Nov 2003 12:59:46 +0000 (12:59 +0000)]
* debugging messages and dumpes commented out

20 years agoPorting to lablgtk2 completed.
Claudio Sacerdoti Coen [Fri, 7 Nov 2003 11:04:17 +0000 (11:04 +0000)]
Porting to lablgtk2 completed.

20 years agoThe hbugs client interface is almost working again.
Claudio Sacerdoti Coen [Fri, 7 Nov 2003 09:34:02 +0000 (09:34 +0000)]
The hbugs client interface is almost working again.

20 years agoHBugs compile again (but it does not do anything right now: still to be
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)

20 years agoFirst release that compiles under lablgtk2 (but it does not work, actually!)
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!)

20 years agoupdated to version 4
Ferruccio Guidi [Wed, 5 Nov 2003 17:33:55 +0000 (17:33 +0000)]
updated to version 4

20 years agoupdated to version 1.4
Ferruccio Guidi [Wed, 5 Nov 2003 10:04:44 +0000 (10:04 +0000)]
updated to version 1.4

20 years ago* first upgrade to the new error logging mechanism
Luca Padovani [Tue, 4 Nov 2003 10:49:02 +0000 (10:49 +0000)]
* first upgrade to the new error logging mechanism

20 years ago*** empty log message ***
Claudio Sacerdoti Coen [Mon, 3 Nov 2003 12:26:51 +0000 (12:26 +0000)]
*** empty log message ***

20 years agosome interfaces changed to prepare the mathql code for version 1.4
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

20 years ago* removed dependency from liblablgtk-ocaml{,-dev}
Luca Padovani [Wed, 29 Oct 2003 10:25:32 +0000 (10:25 +0000)]
* removed dependency from liblablgtk-ocaml{,-dev}

20 years ago* added profiling options
Luca Padovani [Wed, 29 Oct 2003 10:25:04 +0000 (10:25 +0000)]
* added profiling options

20 years ago* temporarily removed hbugs dependency
Luca Padovani [Wed, 29 Oct 2003 10:01:20 +0000 (10:01 +0000)]
* temporarily removed hbugs dependency

20 years ago* updated for gtk2
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

20 years ago* updated for gtk2
Luca Padovani [Wed, 29 Oct 2003 09:59:56 +0000 (09:59 +0000)]
* updated for gtk2

20 years agodebian version 0.0.4-2
Stefano Zacchiroli [Wed, 29 Oct 2003 09:38:22 +0000 (09:38 +0000)]
debian version 0.0.4-2

20 years ago* this implements the new instantiation for gtkmathview
Luca Padovani [Wed, 29 Oct 2003 09:38:09 +0000 (09:38 +0000)]
* this implements the new instantiation for gtkmathview

20 years ago* GEdit -> GText
Luca Padovani [Wed, 29 Oct 2003 09:18:47 +0000 (09:18 +0000)]
* GEdit -> GText

20 years ago* variant types changed for selection mode
Luca Padovani [Wed, 29 Oct 2003 09:17:30 +0000 (09:17 +0000)]
* variant types changed for selection mode

20 years ago* fixed O_S variable for ocamlmklib on hppa arch
Luca Padovani [Tue, 21 Oct 2003 12:50:37 +0000 (12:50 +0000)]
* fixed O_S variable for ocamlmklib on hppa arch

20 years ago- debian release 0.0.6-3
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)

20 years ago* first version of the profile manager committed
Luca Padovani [Tue, 21 Oct 2003 08:28:42 +0000 (08:28 +0000)]
* first version of the profile manager committed

20 years ago* added timer for profiling the editor
Luca Padovani [Sat, 18 Oct 2003 10:42:07 +0000 (10:42 +0000)]
* added timer for profiling the editor

20 years ago* added daemon
Luca Padovani [Fri, 17 Oct 2003 14:01:18 +0000 (14:01 +0000)]
* added daemon
* fixed minor bugs

20 years ago* oo interface
Luca Padovani [Fri, 17 Oct 2003 09:53:46 +0000 (09:53 +0000)]
* oo interface

20 years ago* first files added to cvs
Luca Padovani [Fri, 17 Oct 2003 09:38:12 +0000 (09:38 +0000)]
* first files added to cvs

20 years agodebian version 0.5.1-2
Stefano Zacchiroli [Mon, 13 Oct 2003 07:29:07 +0000 (07:29 +0000)]
debian version 0.5.1-2

20 years agodebian version 0.5.1-1
Stefano Zacchiroli [Mon, 13 Oct 2003 07:14:47 +0000 (07:14 +0000)]
debian version 0.5.1-1

20 years agodebian snapshot version 0.0.6-2
Stefano Zacchiroli [Fri, 10 Oct 2003 07:55:13 +0000 (07:55 +0000)]
debian snapshot version 0.0.6-2

20 years ago* snapshot for gtk2
Luca Padovani [Wed, 8 Oct 2003 06:13:50 +0000 (06:13 +0000)]
* snapshot for gtk2

20 years ago* added new .ml files to be ignored
Luca Padovani [Tue, 7 Oct 2003 17:24:38 +0000 (17:24 +0000)]
* added new .ml files to be ignored

20 years ago* lablgtk -> lablgtk2
Luca Padovani [Tue, 7 Oct 2003 17:20:14 +0000 (17:20 +0000)]
* lablgtk -> lablgtk2

20 years ago* removed debugging Printfs'
Luca Padovani [Tue, 7 Oct 2003 17:18:43 +0000 (17:18 +0000)]
* removed debugging Printfs'

20 years ago* removed currified constructors everywhere. A bug in the ocaml compiler
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 ;-)

20 years agohxp: performes several tasks among which some metadata extraction
Ferruccio Guidi [Mon, 6 Oct 2003 17:25:23 +0000 (17:25 +0000)]
hxp: performes several tasks among which some metadata extraction

20 years ago* minor fix
Luca Padovani [Mon, 6 Oct 2003 09:17:32 +0000 (09:17 +0000)]
* minor fix

20 years ago* removed spec file
Luca Padovani [Mon, 6 Oct 2003 09:05:16 +0000 (09:05 +0000)]
* removed spec file
* updated configuration
* added .props file for lablgtk2

20 years ago* upgrade to lablgtk2
Luca Padovani [Mon, 6 Oct 2003 09:01:48 +0000 (09:01 +0000)]
* upgrade to lablgtk2

20 years ago* checking for lablgtk2
Luca Padovani [Mon, 6 Oct 2003 08:58:47 +0000 (08:58 +0000)]
* checking for lablgtk2

20 years ago* update dependency: lablgtk -> lablgtk2
Luca Padovani [Mon, 6 Oct 2003 08:46:46 +0000 (08:46 +0000)]
* update dependency: lablgtk -> lablgtk2

20 years ago* added popup menu, implemented some functions
Luca Padovani [Sun, 5 Oct 2003 08:02:30 +0000 (08:02 +0000)]
* added popup menu, implemented some functions

20 years agodebian package for ocaml 3.07
Stefano Zacchiroli [Sat, 4 Oct 2003 13:29:11 +0000 (13:29 +0000)]
debian package for ocaml 3.07

20 years ago* changed version in configure.ac
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

20 years ago* further code cleanup
Luca Padovani [Fri, 3 Oct 2003 14:14:51 +0000 (14:14 +0000)]
* further code cleanup

20 years ago* updated #include directives
Luca Padovani [Fri, 3 Oct 2003 14:03:15 +0000 (14:03 +0000)]
* updated #include directives
* clean up of some makefiles

20 years ago* the main function MUST return 0 to communicate everything was OK
Andrea Asperti [Wed, 1 Oct 2003 13:08:08 +0000 (13:08 +0000)]
* the main function MUST return 0 to communicate everything was OK

20 years ago* new version of metadata extraction
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

20 years ago* the regular expressions must have $ otherwise the shortest match
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

20 years ago...
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:41:25 +0000 (17:41 +0000)]
...

20 years agoReindentation.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:40:08 +0000 (17:40 +0000)]
Reindentation.

20 years agoProofEngine.goal := ==> set_proof_engine_goal
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:39:01 +0000 (17:39 +0000)]
ProofEngine.goal :=   ==>   set_proof_engine_goal

20 years agoReindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:33:30 +0000 (17:33 +0000)]
Reindentation

20 years agoProofEngine.proof is now an abstract data type (since we plan to have OMDoc
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).

20 years agopatch
Ferruccio Guidi [Tue, 23 Sep 2003 17:06:50 +0000 (17:06 +0000)]
patch

20 years agoThis version of xmlDiff is much much much smarter than the previous one:
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. ]

20 years agoReindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:58:28 +0000 (15:58 +0000)]
Reindentation

20 years agoBU_Conversion + omit-conclusion is a mess. I have partially fixed the
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.

20 years agoDebugging stuff removed.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:55:28 +0000 (15:55 +0000)]
Debugging stuff removed.

20 years agoNow mathql_generator compiles before mathql_interpreter.
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.

20 years agoPreliminary support for proof-tree enhanced: proof-trees are now shown
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.

20 years ago- added support for proof trees
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

20 years agoclean_cache method added
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 13:00:28 +0000 (13:00 +0000)]
clean_cache method added

20 years agocleancache ==> clean_cache
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:57:01 +0000 (12:57 +0000)]
cleancache ==> clean_cache

20 years agoClean cache method added.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:44:51 +0000 (12:44 +0000)]
Clean cache method added.

20 years agoparam.framewidth = 150 (hard-coded ;-( pour Hanane ;-((((((((((
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 11:58:43 +0000 (11:58 +0000)]
param.framewidth = 150 (hard-coded ;-(    pour Hanane ;-((((((((((

20 years agoFollowing an hyperlink from a proof-tree rendering now brings you to
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.

20 years agoPreliminary commit to support Hanane's proof-tree rendering.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 08:10:14 +0000 (08:10 +0000)]
Preliminary commit to support Hanane's proof-tree rendering.

20 years agoprop.media-type and prop.encoding were _NOT_ considered when the
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.

20 years agowww-sop.inria.fr
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.

20 years ago- bumped copyright years
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

20 years ago- converted TAB to spaces
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:34 +0000 (00:01 +0000)]
- converted TAB to spaces

20 years ago- clear hints list upon status submit
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:25 +0000 (00:01 +0000)]
- clear hints list upon status submit
- converted TAB to spaces

20 years ago- added support for dumping environment to file on exit (disabled by default)
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