]>
 
 
matita.cs.unibo.it Git - helm.git/log 
 
 
 
 
 
 
Claudio Sacerdoti Coen  [Wed, 24 Oct 2001 14:11:25 +0000  (14:11 +0000)] 
 
RDFURI removed because no more unique. 
 
Claudio Sacerdoti Coen  [Wed, 24 Oct 2001 12:44:34 +0000  (12:44 +0000)] 
 
Ported to RDF syntax. 
 
Claudio Sacerdoti Coen  [Wed, 24 Oct 2001 12:43:40 +0000  (12:43 +0000)] 
 
Porting to RDF syntax. 
 
Claudio Sacerdoti Coen  [Wed, 24 Oct 2001 10:35:32 +0000  (10:35 +0000)] 
 
The cache now supports different RDF URI schema at the same time. 
 
Ferruccio Guidi  [Mon, 22 Oct 2001 16:50:56 +0000  (16:50 +0000)] 
 
template mk-mml-op-noannot was modified to allow hidden parameters 
eq and eqT where aligned 
 
Luca Padovani  [Thu, 18 Oct 2001 20:32:41 +0000  (20:32 +0000)] 
 
Initial revision 
 
Claudio Sacerdoti Coen  [Thu, 18 Oct 2001 10:17:15 +0000  (10:17 +0000)] 
 
Bug fixing: now the link to the graphs produce extended URIs 
(e.g. ".../nat.ind#xpointer(1/1/1") 
 
Claudio Sacerdoti Coen  [Thu, 18 Oct 2001 10:11:28 +0000  (10:11 +0000)] 
 
mk_dep_graph.xsl now differentiates the constructors from the 
inductive types producing "extended" URIs 
(e.g. ".../nat.ind#xpointer(1/1/1)") 
 
Claudio Sacerdoti Coen  [Wed, 17 Oct 2001 15:34:43 +0000  (15:34 +0000)] 
 
Oooops. After the last commit all the URLs were damaged. 
 
Stefano Zacchiroli  [Wed, 17 Oct 2001 13:02:20 +0000  (13:02 +0000)] 
 
Makefile.in that support some new architectures. 
 
Claudio Sacerdoti Coen  [Wed, 17 Oct 2001 10:11:56 +0000  (10:11 +0000)] 
 
Bug removed/Feature changed: CIC URIs for inductive data types 
and constructors ending with an #xpointer are now handled 
(more) correctly. 
 
Claudio Sacerdoti Coen  [Tue, 16 Oct 2001 16:53:07 +0000  (16:53 +0000)] 
 
Bug related to #xpointer(1/n/m) constructor URI fixed. 
 
Claudio Sacerdoti Coen  [Mon, 15 Oct 2001 06:17:02 +0000  (06:17 +0000)] 
 
New implementation of the graph stuff: now every hard-coded URL has been 
removed. 
 
Claudio Sacerdoti Coen  [Mon, 15 Oct 2001 06:16:18 +0000  (06:16 +0000)] 
 
Help method added 
 
Claudio Sacerdoti Coen  [Mon, 15 Oct 2001 06:14:13 +0000  (06:14 +0000)] 
 
New implementation of the graphs stuff: now every hard-coded URL has 
been removed. 
 
Claudio Sacerdoti Coen  [Mon, 15 Oct 2001 06:13:10 +0000  (06:13 +0000)] 
 
Commented code removed 
 
Claudio Sacerdoti Coen  [Fri, 12 Oct 2001 08:42:37 +0000  (08:42 +0000)] 
 
New implementation of the graph staff: the logic has been moved 
from mk_html.pl to the stylesheets 
 
Claudio Sacerdoti Coen  [Fri, 12 Oct 2001 08:34:14 +0000  (08:34 +0000)] 
 
New implementation of the graph staff: logic moved 
from mk_html.pl to the stylesheets. 
 
Claudio Sacerdoti Coen  [Tue, 9 Oct 2001 16:42:52 +0000  (16:42 +0000)] 
 
Whoops. Forgot to open the CIC file in the cic window. 
 
Claudio Sacerdoti Coen  [Tue, 9 Oct 2001 16:34:38 +0000  (16:34 +0000)] 
 
Menu in JavaScript substituted to multi-area links. Cool. 
 
Claudio Sacerdoti Coen  [Tue, 9 Oct 2001 15:12:10 +0000  (15:12 +0000)] 
 
Code improvement, same functionalities. 
 
Claudio Sacerdoti Coen  [Mon, 8 Oct 2001 12:03:05 +0000  (12:03 +0000)] 
 
New implementation: now the number of nodes is used to prune the graph 
 
Claudio Sacerdoti Coen  [Mon, 8 Oct 2001 12:01:41 +0000  (12:01 +0000)] 
 
cvsignore added 
 
Claudio Sacerdoti Coen  [Mon, 8 Oct 2001 12:00:27 +0000  (12:00 +0000)] 
 
First release checked in 
 
Claudio Sacerdoti Coen  [Mon, 8 Oct 2001 11:55:24 +0000  (11:55 +0000)] 
 
New graph implementation: the visit is no more pruned on a level base, but 
when the number of the nodes in the graph exceeds a fixed limit. 
 
Claudio Sacerdoti Coen  [Fri, 5 Oct 2001 17:35:13 +0000  (17:35 +0000)] 
 
Debian packaging of helmpot-0.0.3 
 
Claudio Sacerdoti Coen  [Thu, 4 Oct 2001 14:47:27 +0000  (14:47 +0000)] 
 
Many more hard-coded links removed. 
 
Claudio Sacerdoti Coen  [Wed, 3 Oct 2001 15:40:58 +0000  (15:40 +0000)] 
 
First set of hard-coded URLs removed. 
Still many remaining. 
 
Claudio Sacerdoti Coen  [Wed, 3 Oct 2001 15:14:08 +0000  (15:14 +0000)] 
 
Absolute path removed thanks to a bug-fixing in Uwobo. 
To process this stylesheet, a version of Uwobo >= 1.1.11 is required. 
 
Claudio Sacerdoti Coen  [Mon, 1 Oct 2001 09:52:16 +0000  (09:52 +0000)] 
 
First implementation of graphs stuff. Working on my notebook, 
probably not working on-line, yet. 
 
Claudio Sacerdoti Coen  [Mon, 1 Oct 2001 09:46:08 +0000  (09:46 +0000)] 
 
New stylesheets for graphs added 
 
Claudio Sacerdoti Coen  [Mon, 1 Oct 2001 09:40:17 +0000  (09:40 +0000)] 
 
d_c missing 
 
Claudio Sacerdoti Coen  [Mon, 1 Oct 2001 09:37:07 +0000  (09:37 +0000)] 
 
First implementation of graphs. Working on my notebook, probably not 
on-line. 
 
Claudio Sacerdoti Coen  [Fri, 14 Sep 2001 13:58:49 +0000  (13:58 +0000)] 
 
* getter.xsl added 
  In this stylesheet there is a simple function to make the URL 
  of an XML file given its URI. (The URL is used to ask the getter 
  to retrieve the file) 
* every other stylesheet (but ricerca.xsl that is unused and 
  links_library.xsl) has been changed to use the new function 
  instead of computing the URL cutting&pasting the same code 
  again and again. 
 
Luca Padovani  [Wed, 29 Aug 2001 20:30:54 +0000  (20:30 +0000)] 
 
bug fix (helm selection) and new version (sigh) 
 
Claudio Sacerdoti Coen  [Wed, 29 Aug 2001 15:43:47 +0000  (15:43 +0000)] 
 
Proof explosion blocked after lambda-abstractions. 
 
Claudio Sacerdoti Coen  [Wed, 29 Aug 2001 15:16:25 +0000  (15:16 +0000)] 
 
Proof explosion improved (= avoided) for: 
 1) Proofs after lambda-introductions (linear proofs) 
 2) Proofs after a rewriting step (linear proofs) 
 3) Proofs after a letin1 (linear proofs) 
 
Andrea Asperti  [Wed, 29 Aug 2001 11:32:53 +0000  (11:32 +0000)] 
 
1. Fixati alcuni problemi di indentazione con le rewrite. 
2. Esplosione in un colpo solo di catene di riscrittura. 
 
Andrea Asperti  [Tue, 28 Aug 2001 11:12:25 +0000  (11:12 +0000)] 
 
Espansione dinamica delle prove per Mozilla/Galeon. 
 
Claudio Sacerdoti Coen  [Mon, 27 Aug 2001 17:26:05 +0000  (17:26 +0000)] 
 
Upgrade to 0.0.2 
 
Claudio Sacerdoti Coen  [Thu, 23 Aug 2001 13:16:04 +0000  (13:16 +0000)] 
 
* Title added 
* Method onLoad="window.focus()" added. To be removed as soon as the window 
  become a frame. 
 
Claudio Sacerdoti Coen  [Thu, 23 Aug 2001 13:06:10 +0000  (13:06 +0000)] 
 
onLoad="window.focus()" added to every interface window 
In this way, when a link opens a document in another window, that 
window is also raised. 
 
Luca Padovani  [Wed, 22 Aug 2001 12:19:22 +0000  (12:19 +0000)] 
 
configure.in : new version 
 
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