]> matita.cs.unibo.it Git - helm.git/log
helm.git
23 years agoThis commit was manufactured by cvs2svn to create branch 'xmltheory'. xmltheory
no author [Wed, 2 May 2001 14:14:57 +0000 (14:14 +0000)]
This commit was manufactured by cvs2svn to create branch 'xmltheory'.

23 years agoInitial revision
Claudio Sacerdoti Coen [Wed, 2 May 2001 14:14:57 +0000 (14:14 +0000)]
Initial revision

23 years agoregister method added
Claudio Sacerdoti Coen [Thu, 19 Apr 2001 12:13:28 +0000 (12:13 +0000)]
register method added

23 years agoannotationHelper now working again. A control frame has been added to
Claudio Sacerdoti Coen [Wed, 18 Apr 2001 16:03:13 +0000 (16:03 +0000)]
annotationHelper now working again. A control frame has been added to
the CIC or the Theory window to invoke the annotationHelper.

23 years agoWARNING: NOT COMPILING COMMIT
Claudio Sacerdoti Coen [Wed, 18 Apr 2001 10:16:08 +0000 (10:16 +0000)]
WARNING: NOT COMPILING COMMIT

This commit comes from a set of files not in CVS to reingeenere the
whole architecture of the Gtk Interface into an AnnotationHelper,
a ProofChecker and a GtkControl, all independents.

The commit is done just before removing from the AnnotationHelper the
browsing and remote-control features. With this version, the whole
interface does not even compile any more.

23 years agoInitial revision
Luca Padovani [Thu, 12 Apr 2001 15:44:35 +0000 (15:44 +0000)]
Initial revision

23 years agoSome adjustments in the licenses
Luca Padovani [Thu, 12 Apr 2001 13:27:27 +0000 (13:27 +0000)]
Some adjustments in the licenses

Modified Files:
  acconfig.h main.c

23 years agoInitial revision
Luca Padovani [Thu, 12 Apr 2001 11:19:14 +0000 (11:19 +0000)]
Initial revision

23 years agopanel ==> uwobo-panel
Claudio Sacerdoti Coen [Thu, 12 Apr 2001 09:23:15 +0000 (09:23 +0000)]
panel ==> uwobo-panel

23 years agoContent-Cache, Expires and Pragma added for non-error responses.
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:21:06 +0000 (11:21 +0000)]
Content-Cache, Expires and Pragma added for non-error responses.
Should them be there also in case of errors?

23 years agoControl frame added to CIC window
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:05:35 +0000 (11:05 +0000)]
Control frame added to CIC window

23 years agoIn natural language, non vengono piu' stampati glia argomenti
Andrea Asperti [Wed, 11 Apr 2001 11:04:06 +0000 (11:04 +0000)]
In natural language, non vengono piu' stampati glia argomenti
delle applicazioni con sort divers da prop.

23 years agoControl panel added to CIC window
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:03:00 +0000 (11:03 +0000)]
Control panel added to CIC window

23 years agoUnstable commit: just before removing next/prev functionalities
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:00:59 +0000 (11:00 +0000)]
Unstable commit: just before removing next/prev functionalities

23 years agoModified Files:
Irene Schena [Mon, 9 Apr 2001 16:33:00 +0000 (16:33 +0000)]
Modified Files:
1) arith.xsl, contentlib.xsl, reals.xsl, ring.xsl: removed xlink declaration

23 years agocontrol.html, control.js: now commands replace the history, so that
Luca Padovani [Fri, 6 Apr 2001 14:15:26 +0000 (14:15 +0000)]
control.html, control.js: now commands replace the history, so that
the back button in the browser returns immediately to the
previous page (and not the previous command result)

23 years agoAdded URL quoting to quote also "," (required by Netscape for plug-outs)
Claudio Sacerdoti Coen [Fri, 6 Apr 2001 14:05:36 +0000 (14:05 +0000)]
Added URL quoting to quote also "," (required by Netscape for plug-outs)

23 years agoInitial revision
Luca Padovani [Fri, 6 Apr 2001 14:02:02 +0000 (14:02 +0000)]
Initial revision

23 years agocontentlib.xsl improved, now handles eq eqT
Ferruccio Guidi [Thu, 5 Apr 2001 14:57:02 +0000 (14:57 +0000)]
contentlib.xsl improved, now handles eq eqT

23 years agoBug nat_double_ind solved.
Andrea Asperti [Thu, 5 Apr 2001 14:46:12 +0000 (14:46 +0000)]
Bug nat_double_ind solved.

23 years agoBug fixed: the result was declared as gzipped even when it was not so
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 16:01:27 +0000 (16:01 +0000)]
Bug fixed: the result was declared as gzipped even when it was not so

23 years agoImproved rendering for rewriting steps: a little indentation added
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 15:00:00 +0000 (15:00 +0000)]
Improved rendering for rewriting steps: a little indentation added
and a bug in "charcount" called fix.

REMEMBER: charcount mode must be used only on the first child
 because it counts the size of the node considered, its descendants,
 its siblings and all their descendants

23 years agopure ==> proof_transform for the "by" part of rewriting
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 14:31:56 +0000 (14:31 +0000)]
pure ==> proof_transform for the "by" part of rewriting

23 years agopure ==> noannot in CASE's branches
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 14:24:26 +0000 (14:24 +0000)]
pure ==> noannot in CASE's branches

23 years agoBig bug: & was not quoted in the URL for xmluri (that actually always had
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 11:21:35 +0000 (11:21 +0000)]
Big bug: & was not quoted in the URL for xmluri (that actually always had
one)

23 years agofonts for lambda prod and forall enlarged
Ferruccio Guidi [Wed, 4 Apr 2001 10:27:44 +0000 (10:27 +0000)]
fonts for lambda prod and forall enlarged

23 years agocharacters in symbol font unified in size
Ferruccio Guidi [Wed, 4 Apr 2001 09:47:02 +0000 (09:47 +0000)]
characters in symbol font unified in size

23 years agoabstract polinomials
Ferruccio Guidi [Tue, 3 Apr 2001 14:58:57 +0000 (14:58 +0000)]
abstract polinomials

23 years agoadded notations for abstact polinomials
Ferruccio Guidi [Tue, 3 Apr 2001 14:55:36 +0000 (14:55 +0000)]
added notations for abstact polinomials
HTML rendering of constants in symbol font improved (including m:minus)
added a title for the HTML rendering window

23 years agoadded support for HELM_GETTER_URL environment variable
Luca Padovani [Tue, 3 Apr 2001 09:45:18 +0000 (09:45 +0000)]
added support for HELM_GETTER_URL environment variable

23 years agofirst steps towards new interface with UWOBo and new stylesheets
Luca Padovani [Tue, 3 Apr 2001 09:44:28 +0000 (09:44 +0000)]
first steps towards new interface with UWOBo and new stylesheets

23 years agoadded gmon.out
Luca Padovani [Tue, 3 Apr 2001 08:45:28 +0000 (08:45 +0000)]
added gmon.out

23 years ago*** empty log message ***
Andrea Asperti [Tue, 3 Apr 2001 08:18:56 +0000 (08:18 +0000)]
*** empty log message ***

23 years agoLine morally belonging to lablgtk/*.h now is there! Hence, removed
Claudio Sacerdoti Coen [Tue, 3 Apr 2001 07:58:15 +0000 (07:58 +0000)]
Line morally belonging to lablgtk/*.h now is there! Hence, removed

23 years agoComplete management of inductive types.
Andrea Asperti [Tue, 3 Apr 2001 07:56:41 +0000 (07:56 +0000)]
Complete management of inductive types.
or_ind revisited (full_or_in).
(only for html: mml_extension must be upadated!!!).

-- andrea

23 years agoUpdated to lablgtk 1.2 and ocaml-3.01.
Claudio Sacerdoti Coen [Tue, 3 Apr 2001 07:53:51 +0000 (07:53 +0000)]
Updated to lablgtk 1.2 and ocaml-3.01.

23 years agoModified Files:
Irene Schena [Thu, 22 Mar 2001 12:40:20 +0000 (12:40 +0000)]
Modified Files:
1) mmlextension.xsl: added import of mmltheoryextension.xsl
2) objcontent.xsl: added *[1] to apply-templates
Added Files:
1) mmltheoryextension.xsl: MML presentation of objects in theories

23 years agoNow links are followed even in theory + MathML Presentation
Claudio Sacerdoti Coen [Thu, 22 Mar 2001 11:03:12 +0000 (11:03 +0000)]
Now links are followed even in theory + MathML Presentation

23 years agoheadercontent.xsl added to have all the notational stylesheets included in
Claudio Sacerdoti Coen [Wed, 21 Mar 2001 17:53:40 +0000 (17:53 +0000)]
headercontent.xsl added to have all the notational stylesheets included in
the same place

23 years agopatched_dtd => patch_dtd
Claudio Sacerdoti Coen [Wed, 21 Mar 2001 17:37:29 +0000 (17:37 +0000)]
patched_dtd => patch_dtd

23 years agomore notations added
Ferruccio Guidi [Wed, 21 Mar 2001 16:53:40 +0000 (16:53 +0000)]
more notations added

23 years ago- added support for file ls (i.e. you can use a baseuri that point to a
Stefano Zacchiroli [Tue, 20 Mar 2001 17:30:32 +0000 (17:30 +0000)]
- added support for file ls (i.e. you can use a baseuri that point to a
  file with ls)
- change the installcgi method in Makefile, now no error if no cgi is
  going to be installed

23 years agobasic notations for arithmetics
Ferruccio Guidi [Tue, 20 Mar 2001 17:21:14 +0000 (17:21 +0000)]
basic notations for arithmetics

23 years agoadded notation for arithmetics
Ferruccio Guidi [Tue, 20 Mar 2001 17:17:28 +0000 (17:17 +0000)]
added notation for arithmetics

23 years agoChanges in raw mode interface
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 18:05:45 +0000 (18:05 +0000)]
Changes in raw mode interface

23 years agoNow uses the new stylesheets waterfall
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 15:38:30 +0000 (15:38 +0000)]
Now uses the new stylesheets waterfall

23 years agoerror: "iso8859-1" ==> "'iso8859-1'"
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 14:57:42 +0000 (14:57 +0000)]
error: "iso8859-1" ==> "'iso8859-1'"

23 years agomakeURL() and related variables and parameters moved to links_library.xsl
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 14:19:43 +0000 (14:19 +0000)]
makeURL() and related variables and parameters moved to links_library.xsl
prop.* now passed on as param.*

23 years agoModified Files:
Irene Schena [Mon, 19 Mar 2001 12:57:00 +0000 (12:57 +0000)]
Modified Files:
1) expandobj.xsl, link.xsl: changed param media-type

23 years agoModified Files:
Irene Schena [Mon, 19 Mar 2001 12:47:45 +0000 (12:47 +0000)]
Modified Files:
1) theory_pres.xsl: syntax error

23 years agoModified Files:
Irene Schena [Mon, 19 Mar 2001 12:44:17 +0000 (12:44 +0000)]
Modified Files:
1) content_to_html.xsl, expandobj.xsl, html_init.xsl, html_reals.xsl,
html_set.xsl, theory_pres.xsl: now links are uri
Added Files:
1) link.xsl: transformation of uri into url

23 years agoModified Files:
Irene Schena [Mon, 19 Mar 2001 11:46:30 +0000 (11:46 +0000)]
Modified Files:
1) theoryobject.dtd: added theory structure

23 years agogetciconly ==> getxml
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 10:51:12 +0000 (10:51 +0000)]
getciconly ==> getxml

23 years agoModified Files:
Irene Schena [Mon, 19 Mar 2001 10:42:54 +0000 (10:42 +0000)]
Modified Files:
1) expandobj.xsl, params.xsl, theory_content.xsl, theory_pres.xsl: new structurefor theories
2) params.xsl: adding mode="pure" in abstparams
Added Files:
1) objtheorycontent.xsl: new content generation for objects in theories

23 years agoAdded support for CGI handling, still remain some problems for headers,
Stefano Zacchiroli [Sat, 17 Mar 2001 16:10:22 +0000 (16:10 +0000)]
Added support for CGI handling, still remain some problems for headers,
but it works !
- Makefile.in:
  - added some targets like: install and uninstall for getter and cgi
- configure.in
  - added variable substitution for @HELM_CGI_DIR@
- http_getter.pl.in
  - added subroutine html_nice_answer (wrapper for simple html answers)
  - CGI handling when request ends with ".cgi"

23 years agogetciconly ==> getxml
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 18:43:38 +0000 (18:43 +0000)]
getciconly ==> getxml

23 years ago- renamed /getciconly in /getxml
Stefano Zacchiroli [Fri, 16 Mar 2001 18:17:18 +0000 (18:17 +0000)]
- renamed /getciconly in /getxml
- added control on not existent url
- added /resolve method

23 years agoAnnotations now working again (even if in a bit trickier way).
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 17:27:33 +0000 (17:27 +0000)]
Annotations now working again (even if in a bit trickier way).
The get method of the getter could now be safely removed... URRAH!

23 years agoChanged default content type from "text/plain" to "text/xml".
Stefano Zacchiroli [Fri, 16 Mar 2001 17:10:53 +0000 (17:10 +0000)]
Changed default content type from "text/plain" to "text/xml".

23 years agoVarious changes:
Stefano Zacchiroli [Fri, 16 Mar 2001 16:34:24 +0000 (16:34 +0000)]
Various changes:
- added "patch_dtd" parameter to /getciconly method
- removed "remove_header" feature to the download subroutine
- patched response in gz file answering (now use x-gzip encoding header)
- remove /conf method
- removed hard coded "localhost" url

23 years agoRaw mode now really considers compressed/not compressed
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 15:31:10 +0000 (15:31 +0000)]
Raw mode now really considers compressed/not compressed

23 years agoAdded "format" support to /getciconly method.
Stefano Zacchiroli [Fri, 16 Mar 2001 15:10:55 +0000 (15:10 +0000)]
Added "format" support to /getciconly method.
Format may be one of "gz" or "normal", it sets the format of the returned
file either gzipped or uncompressed data.
"format" parameter may also be omitted.

23 years agoMethod get of the getter no more used. Replaced by getciconly
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 13:50:13 +0000 (13:50 +0000)]
Method get of the getter no more used. Replaced by getciconly
(whose name is now insignificant)

23 years agoehm ... no comment
Stefano Zacchiroli [Fri, 16 Mar 2001 13:39:11 +0000 (13:39 +0000)]
ehm ... no comment

23 years agoFixed a bug in the case cachemode=gzipped, resourcetype=normal.
Stefano Zacchiroli [Fri, 16 Mar 2001 12:26:51 +0000 (12:26 +0000)]
Fixed a bug in the case cachemode=gzipped, resourcetype=normal.
(note: it's time to adopt "use strict" in http_getter.pl !!!!)

23 years agoFiles with annotations available now use a different icon
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:48:37 +0000 (11:48 +0000)]
Files with annotations available now use a different icon

23 years agoUsed for files where annotations are availables
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:43:18 +0000 (11:43 +0000)]
Used for files where annotations are availables

23 years agoannotations now taken in account (as was for naturalLanguage)
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:36:14 +0000 (11:36 +0000)]
annotations now taken in account (as was for naturalLanguage)

23 years agoFixed bug in .ann extension handling.
Stefano Zacchiroli [Fri, 16 Mar 2001 10:44:21 +0000 (10:44 +0000)]
Fixed bug in .ann extension handling.

23 years agoSyntax error + new indenting
Claudio Sacerdoti Coen [Wed, 14 Mar 2001 16:17:22 +0000 (16:17 +0000)]
Syntax error + new indenting

23 years agoConfiguration on-line now pass the parameters
Claudio Sacerdoti Coen [Wed, 14 Mar 2001 16:17:08 +0000 (16:17 +0000)]
Configuration on-line now pass the parameters

23 years agoInitial revision
Luca Padovani [Tue, 13 Mar 2001 09:12:56 +0000 (09:12 +0000)]
Initial revision

23 years agoLast update before dismission
Claudio Sacerdoti Coen [Mon, 12 Mar 2001 17:37:12 +0000 (17:37 +0000)]
Last update before dismission

23 years agoAdded dtd reference in ls method while generating xml output.
Stefano Zacchiroli [Sat, 10 Mar 2001 11:25:36 +0000 (11:25 +0000)]
Added dtd reference in ls method while generating xml output.

23 years agoModified Files:
Irene Schena [Fri, 9 Mar 2001 15:04:38 +0000 (15:04 +0000)]
Modified Files:
1) expandobj.xsl: comments
2) objcontent.xsl, params.xsl: parameters abstraction from objcontent to params

23 years agoModified Files:
Irene Schena [Fri, 9 Mar 2001 11:27:39 +0000 (11:27 +0000)]
Modified Files:
1) content_to_html.xsl: removed mtext, modified output and added
naturalLanguage
2) theory_content.xsl: generate only content markup for theories
3) theory_pres.xsl: generate only html pres for theories, starting
from the corresponding content markup
Added Files:
1) expandobj.xsl: expand objects generating the corresponding content
markup or the pres one, starting from the markup for theories

23 years agothe version command has been renamed into help, the syntax of the available
Luca Padovani [Thu, 8 Mar 2001 11:05:21 +0000 (11:05 +0000)]
the version command has been renamed into help, the syntax of the available
commands will be added soon

23 years agoprocessorURL must now already end with a /
Claudio Sacerdoti Coen [Wed, 7 Mar 2001 17:06:39 +0000 (17:06 +0000)]
processorURL must now already end with a /

23 years agoNow the on-line interface can use a Getter and an UWOBO on any machine
Claudio Sacerdoti Coen [Wed, 7 Mar 2001 17:02:42 +0000 (17:02 +0000)]
Now the on-line interface can use a Getter and an UWOBO on any machine

23 years agoBug fixed: now propagates informations about inner-types usage and
Claudio Sacerdoti Coen [Wed, 7 Mar 2001 11:05:20 +0000 (11:05 +0000)]
Bug fixed: now propagates informations about inner-types usage and
natural language when following hyperlinks.

WARNING: to create an hyperlink, it is no more enough to concatenate
 $header and the URI. You need to call the new makeURL() named-template.

23 years ago*** empty log message ***
Andrea Asperti [Wed, 7 Mar 2001 08:40:27 +0000 (08:40 +0000)]
*** empty log message ***

23 years agogetter flags considered
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 18:47:08 +0000 (18:47 +0000)]
getter flags considered

23 years agoAdded ordering in ann and types flags
Stefano Zacchiroli [Tue, 6 Mar 2001 17:12:25 +0000 (17:12 +0000)]
Added ordering in ann and types flags

23 years agolibrary3 ==> javascript
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 16:10:16 +0000 (16:10 +0000)]
library3 ==> javascript

23 years agoNew on-line interface
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 16:06:36 +0000 (16:06 +0000)]
New on-line interface

23 years agoNew online interface
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 16:05:57 +0000 (16:05 +0000)]
New online interface

23 years agoThe .types files are now read directly by the stylesheets.
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 16:00:32 +0000 (16:00 +0000)]
The .types files are now read directly by the stylesheets.
Two new params added: naturalLanguage and CICURI

23 years agoNow uses the param keys
Claudio Sacerdoti Coen [Tue, 6 Mar 2001 15:01:43 +0000 (15:01 +0000)]
Now uses the param keys

23 years agonew version of ls,
Stefano Zacchiroli [Mon, 5 Mar 2001 21:15:47 +0000 (21:15 +0000)]
new version of ls,
now meet the specifications ?????

23 years agoadded eq_ind
Andrea Asperti [Mon, 5 Mar 2001 12:30:52 +0000 (12:30 +0000)]
added eq_ind

23 years agoFixed a bug in CGI creation, method "update" now work ! :)
Stefano Zacchiroli [Mon, 5 Mar 2001 10:31:12 +0000 (10:31 +0000)]
Fixed a bug in CGI creation, method "update" now work ! :)

23 years agopatch for libxml2 new release
Luca Padovani [Thu, 1 Mar 2001 12:38:29 +0000 (12:38 +0000)]
patch for libxml2 new release

23 years agoWebEQ definitely no more used
Claudio Sacerdoti Coen [Thu, 1 Mar 2001 11:27:14 +0000 (11:27 +0000)]
WebEQ definitely no more used

23 years agoChanged syntax for 'ls' method:
Stefano Zacchiroli [Thu, 22 Feb 2001 14:21:44 +0000 (14:21 +0000)]
Changed syntax for 'ls' method:
  wget http....localhost:8081/ls?baseuri=<uri>&format=[txt|xml]
Now is possibile to:
 - use ls for 'cic:' uris
 - use ls for 'theory:' uris
 - coming soon support for 'any' uris
Now getter use CGI module, added this dep. to configure.in

23 years agocommented processing instructions for Cocoon, we do not use it any more
Luca Padovani [Thu, 22 Feb 2001 09:52:05 +0000 (09:52 +0000)]
commented processing instructions for Cocoon, we do not use it any more

23 years agonow do unescaping of incoming URI
Luca Padovani [Wed, 21 Feb 2001 18:24:10 +0000 (18:24 +0000)]
now do unescaping of incoming URI

23 years agoadded the patch on-the-fly for DTDs, fixed the script for launching the getter at...
Luca Padovani [Wed, 21 Feb 2001 15:11:23 +0000 (15:11 +0000)]
added the patch on-the-fly for DTDs, fixed the script for launching the getter at boot time

23 years agoNew stylesheets from content to html.
Andrea Asperti [Tue, 20 Feb 2001 10:30:36 +0000 (10:30 +0000)]
New stylesheets from content to html.

-- andrea

23 years agoAdded 'ls' method: return a list of uri that begin with a given uri.
Stefano Zacchiroli [Sat, 17 Feb 2001 23:02:10 +0000 (23:02 +0000)]
Added 'ls' method: return a list of uri that begin with a given uri.
Response may be in CR-separated line or in a simple XML document.

23 years agohelm_wget subroutine now use LWP module and doesn't use any more external
Stefano Zacchiroli [Sat, 17 Feb 2001 21:03:06 +0000 (21:03 +0000)]
helm_wget subroutine now use LWP module and doesn't use any more external
wget program