]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Wed, 20 Jun 2001 10:34:44 +0000 (10:34 +0000)]
UNICODEvsSYMBOL parameter added to select the old
<FONT FACE="symbol".../> way of getting mathematical symbol
vs simply using UNICODE entities.
Only a very small percentage of stylesheets (notably part of
content_to_html.xsl and all of html_set.xsl) has been modified to
take into account the new variable.
Claudio Sacerdoti Coen [Mon, 18 Jun 2001 14:06:32 +0000 (14:06 +0000)]
drop_coercions added
Andrea Asperti [Mon, 18 Jun 2001 10:23:38 +0000 (10:23 +0000)]
BUG LAMBDA fixed.
Andrea Asperti [Mon, 18 Jun 2001 10:22:55 +0000 (10:22 +0000)]
drop_coercions.xsl has been added
Claudio Sacerdoti Coen [Mon, 11 Jun 2001 13:37:56 +0000 (13:37 +0000)]
Default for patch_dtd modified to "yes".
Claudio Sacerdoti Coen [Mon, 4 Jun 2001 17:47:01 +0000 (17:47 +0000)]
xsl:import to cope with new xalan version
Claudio Sacerdoti Coen [Tue, 15 May 2001 13:11:10 +0000 (13:11 +0000)]
****
WARNING: unstable commit
****
We are just in the middle of the splitting of mmlinterface into
* annotationHelper
* controlInterface
* proof-checker
All the executables but mmlinterface are now compiling and
working (but the proof-checker that is still V6-bound).
Andrea Asperti [Tue, 15 May 2001 09:35:51 +0000 (09:35 +0000)]
Aggiunto lambda.xsl
Andrea Asperti [Tue, 15 May 2001 09:31:15 +0000 (09:31 +0000)]
Lambda notazione.
Irene Schena [Thu, 10 May 2001 14:19:48 +0000 (14:19 +0000)]
Modified Files:
1) maththeory.dtd, theoryobject.dtd: new structure for xml and content theories
Claudio Sacerdoti Coen [Wed, 9 May 2001 14:40:58 +0000 (14:40 +0000)]
URI may now have #
Claudio Sacerdoti Coen [Wed, 9 May 2001 14:15:18 +0000 (14:15 +0000)]
URIs containing # are now threaded in the "right" way,
which is
The #-part is removed, the URL to uwobo is generated and
the removed #-part is appended to the computed URL.
Note: in this way the #-part is not passed to the getter and then
back to the source. For a #-part this seems reasonable, but could
not work with CGIs looking to the #-part. (Do they exist?)
Claudio Sacerdoti Coen [Wed, 9 May 2001 13:27:56 +0000 (13:27 +0000)]
Attribute @name of ENTITY removed.
Claudio Sacerdoti Coen [Tue, 8 May 2001 11:20:26 +0000 (11:20 +0000)]
Many improvements in theory-rendering.
In particular, now param.type may be 'standalone' or 'typeonly' or 'embed'.
(It was 0 or 1 before)
Modified Files:
content_to_html.xsl expandobj.xsl links_library.xsl
mmlextension.xsl objtheorycontent.xsl theory_content.xsl
theory_pres.xsl
Claudio Sacerdoti Coen [Mon, 7 May 2001 15:01:39 +0000 (15:01 +0000)]
Relative anchors (#xxx) should be followed _inside_ the current document.
Luca Padovani [Sun, 6 May 2001 12:30:47 +0000 (12:30 +0000)]
minidom.c : fixed memory leak
Claudio Sacerdoti Coen [Fri, 4 May 2001 14:54:30 +0000 (14:54 +0000)]
New standard stylesheet genmmlid.xsl added.
Claudio Sacerdoti Coen [Fri, 4 May 2001 14:53:47 +0000 (14:53 +0000)]
New version of Igor Rodionov stylesheets.
Irene Schena [Fri, 4 May 2001 14:14:05 +0000 (14:14 +0000)]
Modified Files:
1) link.xsl: recover linking info and remove mml content
2) mmlextension.xsl: added mrows and import of mmlctop.xsl-0.14
Added Files:
1) genmmlid.xsl: generate ids for mml elements
2) mmlctop.xsl-0.14: new stylesheet of Rodionov
Removed Files:
1) mml2mmlv1_0.xsl: old stylesheet of Rodionov
Claudio Sacerdoti Coen [Fri, 4 May 2001 11:44:50 +0000 (11:44 +0000)]
':' are noc quoted. I tried to quote them, but everything else
broke down (and I don't really understand why: maybe we need
to decode something or uwobo gives the stylesheet a quoted URL?)
Claudio Sacerdoti Coen [Fri, 4 May 2001 10:46:20 +0000 (10:46 +0000)]
Stylesheets for (cic|content|presentation) theory now fully working
Claudio Sacerdoti Coen [Fri, 4 May 2001 09:15:55 +0000 (09:15 +0000)]
Bug fixed: following a link to an object inside a theory opened the
object with the header of the theories.
Claudio Sacerdoti Coen [Fri, 4 May 2001 09:14:45 +0000 (09:14 +0000)]
Bug fixed: following a link to an object inside a theory opened the object
with the header of the theories.
Claudio Sacerdoti Coen [Fri, 4 May 2001 09:13:53 +0000 (09:13 +0000)]
Links not starting with cic: or theory: are now left untouched and
open a new _blank window
Irene Schena [Thu, 3 May 2001 18:03:10 +0000 (18:03 +0000)]
Theory level DTD changed and .theory.xml files exported again.
Working only for HTML and MathML presentation.
Modified Files:
expandobj.xsl link.xsl links_library.xsl theory_content.xsl
theory_pres.xsl
Claudio Sacerdoti Coen [Wed, 2 May 2001 14:21:35 +0000 (14:21 +0000)]
.cvsignore files missing
Claudio Sacerdoti Coen [Wed, 2 May 2001 14:14:57 +0000 (14:14 +0000)]
Initial revision
Claudio Sacerdoti Coen [Thu, 19 Apr 2001 12:13:28 +0000 (12:13 +0000)]
register method added
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.
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.
Luca Padovani [Thu, 12 Apr 2001 15:44:35 +0000 (15:44 +0000)]
Initial revision
Luca Padovani [Thu, 12 Apr 2001 13:27:27 +0000 (13:27 +0000)]
Some adjustments in the licenses
Modified Files:
acconfig.h main.c
Luca Padovani [Thu, 12 Apr 2001 11:19:14 +0000 (11:19 +0000)]
Initial revision
Claudio Sacerdoti Coen [Thu, 12 Apr 2001 09:23:15 +0000 (09:23 +0000)]
panel ==> uwobo-panel
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?
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:05:35 +0000 (11:05 +0000)]
Control frame added to CIC window
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.
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:03:00 +0000 (11:03 +0000)]
Control panel added to CIC window
Claudio Sacerdoti Coen [Wed, 11 Apr 2001 11:00:59 +0000 (11:00 +0000)]
Unstable commit: just before removing next/prev functionalities
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
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)
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)
Luca Padovani [Fri, 6 Apr 2001 14:02:02 +0000 (14:02 +0000)]
Initial revision
Ferruccio Guidi [Thu, 5 Apr 2001 14:57:02 +0000 (14:57 +0000)]
contentlib.xsl improved, now handles eq eqT
Andrea Asperti [Thu, 5 Apr 2001 14:46:12 +0000 (14:46 +0000)]
Bug nat_double_ind solved.
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
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
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 14:31:56 +0000 (14:31 +0000)]
pure ==> proof_transform for the "by" part of rewriting
Claudio Sacerdoti Coen [Wed, 4 Apr 2001 14:24:26 +0000 (14:24 +0000)]
pure ==> noannot in CASE's branches
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)
Ferruccio Guidi [Wed, 4 Apr 2001 10:27:44 +0000 (10:27 +0000)]
fonts for lambda prod and forall enlarged
Ferruccio Guidi [Wed, 4 Apr 2001 09:47:02 +0000 (09:47 +0000)]
characters in symbol font unified in size
Ferruccio Guidi [Tue, 3 Apr 2001 14:58:57 +0000 (14:58 +0000)]
abstract 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
Luca Padovani [Tue, 3 Apr 2001 09:45:18 +0000 (09:45 +0000)]
added support for HELM_GETTER_URL environment variable
Luca Padovani [Tue, 3 Apr 2001 09:44:28 +0000 (09:44 +0000)]
first steps towards new interface with UWOBo and new stylesheets
Luca Padovani [Tue, 3 Apr 2001 08:45:28 +0000 (08:45 +0000)]
added gmon.out
Andrea Asperti [Tue, 3 Apr 2001 08:18:56 +0000 (08:18 +0000)]
*** empty log message ***
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
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
Claudio Sacerdoti Coen [Tue, 3 Apr 2001 07:53:51 +0000 (07:53 +0000)]
Updated to lablgtk 1.2 and ocaml-3.01.
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
Claudio Sacerdoti Coen [Thu, 22 Mar 2001 11:03:12 +0000 (11:03 +0000)]
Now links are followed even in theory + MathML Presentation
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
Claudio Sacerdoti Coen [Wed, 21 Mar 2001 17:37:29 +0000 (17:37 +0000)]
patched_dtd => patch_dtd
Ferruccio Guidi [Wed, 21 Mar 2001 16:53:40 +0000 (16:53 +0000)]
more notations added
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
Ferruccio Guidi [Tue, 20 Mar 2001 17:21:14 +0000 (17:21 +0000)]
basic notations for arithmetics
Ferruccio Guidi [Tue, 20 Mar 2001 17:17:28 +0000 (17:17 +0000)]
added notation for arithmetics
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 18:05:45 +0000 (18:05 +0000)]
Changes in raw mode interface
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 15:38:30 +0000 (15:38 +0000)]
Now uses the new stylesheets waterfall
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 14:57:42 +0000 (14:57 +0000)]
error: "iso8859-1" ==> "'iso8859-1'"
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.*
Irene Schena [Mon, 19 Mar 2001 12:57:00 +0000 (12:57 +0000)]
Modified Files:
1) expandobj.xsl, link.xsl: changed param media-type
Irene Schena [Mon, 19 Mar 2001 12:47:45 +0000 (12:47 +0000)]
Modified Files:
1) theory_pres.xsl: syntax error
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
Irene Schena [Mon, 19 Mar 2001 11:46:30 +0000 (11:46 +0000)]
Modified Files:
1) theoryobject.dtd: added theory structure
Claudio Sacerdoti Coen [Mon, 19 Mar 2001 10:51:12 +0000 (10:51 +0000)]
getciconly ==> getxml
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
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"
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 18:43:38 +0000 (18:43 +0000)]
getciconly ==> 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
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!
Stefano Zacchiroli [Fri, 16 Mar 2001 17:10:53 +0000 (17:10 +0000)]
Changed default content type from "text/plain" to "text/xml".
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
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 15:31:10 +0000 (15:31 +0000)]
Raw mode now really considers compressed/not compressed
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.
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)
Stefano Zacchiroli [Fri, 16 Mar 2001 13:39:11 +0000 (13:39 +0000)]
ehm ... no comment
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 !!!!)
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:48:37 +0000 (11:48 +0000)]
Files with annotations available now use a different icon
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:43:18 +0000 (11:43 +0000)]
Used for files where annotations are availables
Claudio Sacerdoti Coen [Fri, 16 Mar 2001 11:36:14 +0000 (11:36 +0000)]
annotations now taken in account (as was for naturalLanguage)
Stefano Zacchiroli [Fri, 16 Mar 2001 10:44:21 +0000 (10:44 +0000)]
Fixed bug in .ann extension handling.
Claudio Sacerdoti Coen [Wed, 14 Mar 2001 16:17:22 +0000 (16:17 +0000)]
Syntax error + new indenting
Claudio Sacerdoti Coen [Wed, 14 Mar 2001 16:17:08 +0000 (16:17 +0000)]
Configuration on-line now pass the parameters
Luca Padovani [Tue, 13 Mar 2001 09:12:56 +0000 (09:12 +0000)]
Initial revision
Claudio Sacerdoti Coen [Mon, 12 Mar 2001 17:37:12 +0000 (17:37 +0000)]
Last update before dismission
Stefano Zacchiroli [Sat, 10 Mar 2001 11:25:36 +0000 (11:25 +0000)]
Added dtd reference in ls method while generating xml output.
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