]>
matita.cs.unibo.it Git - helm.git/log
Irene Schena [Fri, 27 Jul 2001 10:06:04 +0000 (10:06 +0000)]
Modified Files:
1) mmlextension.xsl: m:xref fixed
Irene Schena [Fri, 27 Jul 2001 09:58:57 +0000 (09:58 +0000)]
----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: m:xref fixed
----------------------------------------------------------------------
Irene Schena [Thu, 26 Jul 2001 15:49:26 +0000 (15:49 +0000)]
----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: added notation for lambda calculus
----------------------------------------------------------------------
Irene Schena [Thu, 26 Jul 2001 11:52:34 +0000 (11:52 +0000)]
----------------------------------------------------------------------
Modified Files:
1) content_to_html.xsl html_init.xsl html_reals.xsl html_set.xsl: added
control on the existence of definitionURL
----------------------------------------------------------------------
Andrea Asperti [Thu, 26 Jul 2001 09:02:17 +0000 (09:02 +0000)]
Bug in zarith notation corrected.
Irene Schena [Wed, 25 Jul 2001 13:55:18 +0000 (13:55 +0000)]
----------------------------------------------------------------------
Modified Files:
1) content_to_html.xsl: bug fixed
----------------------------------------------------------------------
Irene Schena [Wed, 25 Jul 2001 12:16:02 +0000 (12:16 +0000)]
----------------------------------------------------------------------
Modified Files:
1) content.xsl content_to_html.xsl mmlextension.xsl: added MML
piecewise for Mutcase patterns
----------------------------------------------------------------------
Andrea Asperti [Wed, 25 Jul 2001 08:55:25 +0000 (08:55 +0000)]
"Recursive" notation for Z.
Irene Schena [Tue, 24 Jul 2001 16:12:47 +0000 (16:12 +0000)]
----------------------------------------------------------------------
Modified Files:
1) mmlctop.xsl-0.14, mmlextension.xsl: changed mchar into entities and
formatted new proof elements.
----------------------------------------------------------------------
Claudio Sacerdoti Coen [Mon, 23 Jul 2001 12:01:43 +0000 (12:01 +0000)]
Fixed a problem of Netscape with 'file:///' URL.
Now the stylesheets are copied inside every HTML file instead of
creating a <link/> to them.
Claudio Sacerdoti Coen [Fri, 20 Jul 2001 15:19:31 +0000 (15:19 +0000)]
First version using maction/toggle to navigate proofs.
Claudio Sacerdoti Coen [Fri, 20 Jul 2001 15:14:18 +0000 (15:14 +0000)]
Added explodeall parameter (default="false") to generate mactions with
only the exploded component. Used during annotation.
Claudio Sacerdoti Coen [Fri, 20 Jul 2001 14:47:23 +0000 (14:47 +0000)]
Metadata were broken in MathML presentation mode.
Claudio Sacerdoti Coen [Thu, 19 Jul 2001 16:52:13 +0000 (16:52 +0000)]
First partial syncronization between the HTML and the MathML presentation:
many csymbols added to MathML presentation.
*** NOTE! ***
The code seems to work perfectly, but I am unsure it is well implemented.
It is better to have a thorough look at it as soon as possible.
*************
The syncronization is still incomplete. The following csymbols are
missing (all of them from the Huet contrib):
subst
lift lift_with_base
beta_red1
beta_red
par_beta_red1
par_beta_red
forgetful
isomorphic
interp
Luca Padovani [Tue, 17 Jul 2001 13:47:13 +0000 (13:47 +0000)]
added preliminary support for maction
- cursor bug
Claudio Sacerdoti Coen [Mon, 16 Jul 2001 12:38:10 +0000 (12:38 +0000)]
Two parameters used but not declared. Fixed.
Andrea Asperti [Thu, 5 Jul 2001 09:27:20 +0000 (09:27 +0000)]
Notation for ZArith (inside arith.xsl) added.
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 15:16:28 +0000 (15:16 +0000)]
drop_coercion (d_c) inserted in every stylesheet chain
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 14:59:04 +0000 (14:59 +0000)]
mk_meta_theory.xsl added
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 14:56:54 +0000 (14:56 +0000)]
Makefile fixed (too many parameters on command line);
xslt/occurrences.xsl added
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 14:51:48 +0000 (14:51 +0000)]
topurl parameter now passed around
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 14:33:49 +0000 (14:33 +0000)]
First completely working interface for metadata.
Andrea Asperti [Fri, 29 Jun 2001 14:05:12 +0000 (14:05 +0000)]
":" bug in theory_pres fixed.
Andrea Asperti [Fri, 29 Jun 2001 13:36:53 +0000 (13:36 +0000)]
small error inside mk_meta_theory.
Andrea Asperti [Fri, 29 Jun 2001 12:57:12 +0000 (12:57 +0000)]
mk_meta_theory.xsl added
It generates a theory starting from metadata.
Andrea Asperti [Fri, 29 Jun 2001 12:55:50 +0000 (12:55 +0000)]
occurrences.xsl added
It computes all occurrences of identifiers inside a given document.
It is used for computing metadata.
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 11:14:59 +0000 (11:14 +0000)]
ht:OBJECT added;
ls.dtd added
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 11:14:38 +0000 (11:14 +0000)]
ht:OBJECT added
Claudio Sacerdoti Coen [Fri, 29 Jun 2001 10:09:48 +0000 (10:09 +0000)]
Total compatibility with Mozilla 9.1 reached with this commit.
Claudio Sacerdoti Coen [Thu, 28 Jun 2001 12:00:51 +0000 (12:00 +0000)]
.cvsignore added
Claudio Sacerdoti Coen [Thu, 28 Jun 2001 11:48:48 +0000 (11:48 +0000)]
CIC files are now processed one by one once given the list of their
URIs (that will be soon provided by a new getter method)
Claudio Sacerdoti Coen [Wed, 27 Jun 2001 17:44:41 +0000 (17:44 +0000)]
First version of metadata interface.
Still many things to be fixed and one stylesheet (of Andrea) not committed.
But it is a new beginning...
Claudio Sacerdoti Coen [Wed, 27 Jun 2001 13:11:05 +0000 (13:11 +0000)]
Repository created.
Stefano Zacchiroli [Wed, 27 Jun 2001 09:14:34 +0000 (09:14 +0000)]
added support for new environment variables
- HTTP_GETTER_RDF_DIR, cache dir for rdf metadata
- HTTP_GETTER_RDF_DBM, dbm file that map rdf uri to url _without_ .db ext
- HTTP_GETTER_RDF_INDEXNAME, name of the indexfile that contain rdf index
Stefano Zacchiroli [Wed, 27 Jun 2001 07:07:02 +0000 (07:07 +0000)]
# bugfix: rdf tie that proxies rdf_urls_of_uris.db now works even after
invocation of /update method
Stefano Zacchiroli [Tue, 26 Jun 2001 16:12:32 +0000 (16:12 +0000)]
added useful tools for perl debugging:
- tools/dump_db.pl => print out a dump of a .db file
- tools/uri_escape.pl => escape a URI
- tools/uri_unescape.pl => unescape a URI
very little things, but really useful!
Claudio Sacerdoti Coen [Tue, 26 Jun 2001 15:58:21 +0000 (15:58 +0000)]
Format of rdf URIs relaxed
Claudio Sacerdoti Coen [Tue, 26 Jun 2001 15:12:14 +0000 (15:12 +0000)]
Version modified
Claudio Sacerdoti Coen [Tue, 26 Jun 2001 15:11:26 +0000 (15:11 +0000)]
Now helm:rdf:... is a valid URI.
Before it had to be helm:rdf/:...
Stefano Zacchiroli [Tue, 26 Jun 2001 14:48:51 +0000 (14:48 +0000)]
* added preliminary support for rdf metadata
- "getxml" method return also rdf metadata
- "update" method update both urls_of_uris and rdf db
- "resolve" method resolve both normal and rdf uris
* added sub isRdfUri
* added sub resolve
* changed VERSION var in configure.in, now in sync with cvs repository
version .. :-)
Claudio Sacerdoti Coen [Tue, 26 Jun 2001 12:38:58 +0000 (12:38 +0000)]
UNICODEvsSYMBOL introduced everywhere. (work completed)
Claudio Sacerdoti Coen [Mon, 25 Jun 2001 17:56:34 +0000 (17:56 +0000)]
UNICODEvsSYMBOL introduced
Claudio Sacerdoti Coen [Mon, 25 Jun 2001 17:02:53 +0000 (17:02 +0000)]
Bug fixed: Compressed was not checked well on control frame load.
"yes" ==> "compressed"
Claudio Sacerdoti Coen [Mon, 25 Jun 2001 10:03:34 +0000 (10:03 +0000)]
Comment removed because XSLT removed the "end-of-line" after it, making it
extends too much, commenting out the following lines. ;-(
Claudio Sacerdoti Coen [Mon, 25 Jun 2001 09:52:36 +0000 (09:52 +0000)]
"Bug" appearing under IE only fixed.
Claudio Sacerdoti Coen [Fri, 22 Jun 2001 16:35:07 +0000 (16:35 +0000)]
Many modifications to avoid JavaScript security rules of
Mozilla/Galeon/Netscape V6 browsers.
In particular, now every frame (but the two headers that are completely
dummy) is made by UWOBO. The stylesheet applied, named resolve_topurl.xsl
(key = RT) substitutes where requested the URL of the interface, that
can no longer be inferred in JavaScript from the current URL (that now
refers to UWOBO).
Hopefully, together with the previous modification to recognize browsers
supporting only UNICODE or supporting only the symbol font, all the
known compatibility problems have been solved.
Claudio Sacerdoti Coen [Fri, 22 Jun 2001 16:29:57 +0000 (16:29 +0000)]
resolve_topurl.xsl added
Claudio Sacerdoti Coen [Fri, 22 Jun 2001 10:48:59 +0000 (10:48 +0000)]
Some simplifications (redundant code).
Claudio Sacerdoti Coen [Fri, 22 Jun 2001 10:37:59 +0000 (10:37 +0000)]
top.topurl alias topurl alias interfaceURL alias thinterfaceURL is no
more "http://phd.cs.unibo.it/helm/library/index.html", but
only "http://phd.cs.unibo.it/helm"
Claudio Sacerdoti Coen [Wed, 20 Jun 2001 13:31:46 +0000 (13:31 +0000)]
UNICODEvsSYMBOL parameter now added everywhere
Claudio Sacerdoti Coen [Wed, 20 Jun 2001 12:09:37 +0000 (12:09 +0000)]
Small bugs fixed:
mathcolor ==> color in <FONT>
arrow size set equal to "+0"
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