]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Tue, 6 Nov 2001 12:35:51 +0000 (12:35 +0000)]
Commit of Ferruccio changes:
* New syntax: every method now accepts a list of inputs
* Small bug fixes
Andrea Asperti [Mon, 5 Nov 2001 09:06:40 +0000 (09:06 +0000)]
Algebra notation.
Claudio Sacerdoti Coen [Mon, 5 Nov 2001 08:56:25 +0000 (08:56 +0000)]
Small bug fixed:
* xsl-import not first instruction
* $id ==> @id
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:59:30 +0000 (13:59 +0000)]
Simple stylesheet for Dublin Core Metadata rendering.
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:32:57 +0000 (13:32 +0000)]
Dublin Core Metadata rendering added.
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:32:34 +0000 (13:32 +0000)]
Very simple stylesheet to render Dublin Core Metadata.
Claudio Sacerdoti Coen [Mon, 29 Oct 2001 15:56:54 +0000 (15:56 +0000)]
backpointer ==> backPointer
Claudio Sacerdoti Coen [Sun, 28 Oct 2001 22:48:19 +0000 (22:48 +0000)]
New copyright free implementation of menus in JavaScript.
Claudio Sacerdoti Coen [Sun, 28 Oct 2001 22:46:32 +0000 (22:46 +0000)]
BUG Fixed: arcs with attributes were not processed in the right way.
Claudio Sacerdoti Coen [Fri, 26 Oct 2001 12:14:14 +0000 (12:14 +0000)]
Some comments added.
Claudio Sacerdoti Coen [Fri, 26 Oct 2001 12:12:10 +0000 (12:12 +0000)]
Problem of URLs too long for I.E. avoided by removing an unuseful parameter
from the inner URL to create a graph. It seems to work for now...
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 17:16:40 +0000 (17:16 +0000)]
Small bug: the theory was open in the graph windows instead of its own.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:44:28 +0000 (16:44 +0000)]
Forward and backward metadata added to the Raw menu.
OPEN BUG: asking metadata for inductive types does not work. A window
requesting which metadata to show should be opened instead.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:36:04 +0000 (16:36 +0000)]
There were still many problems with URIs with a ' in the middle.
Now they should be all resolved (in theory, at least ;-)
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:07:49 +0000 (16:07 +0000)]
Also starting from metadatas it is now possible to select the number
of nodes.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 13:14:47 +0000 (13:14 +0000)]
Clicking on the AREA and not on the menu just pop-ups the menu again instead
of crashing.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 11:59:16 +0000 (11:59 +0000)]
BUG FIXED: URIs with a ' in the middle do not create problems any more.
[Note: We now have problems with URIs with a " in the middle ;-)]
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:54:43 +0000 (10:54 +0000)]
A -> B now means "A depends on B" both in backward and forward graphs
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:31:33 +0000 (10:31 +0000)]
A link to the theory of backward dependencies added to the menu.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:27:01 +0000 (10:27 +0000)]
The code to create a link to the theory automatically generated from the
backward metadata has been moved here from metadataLib.xsl.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:26:24 +0000 (10:26 +0000)]
Code clean-up: the code to create the link to the theory automatically
generated from the backward metadata has been moved to makeGraphLinks.js
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:20:58 +0000 (10:20 +0000)]
The JavaScript code is now defined in on-line/javascript/graphLinks.xsl and
it is shared with medataLib.xsl.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:19:53 +0000 (10:19 +0000)]
Code obtained from the factorization of makeGraphLinks.xsl and metadataLib.xsl
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 09:45:52 +0000 (09:45 +0000)]
Oooops. I have exchanged the targets of the links to the graphs of
forward and backward dependencies. Fixed.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 17:31:32 +0000 (17:31 +0000)]
Code to share with makeGraphLinks.xsl extracted to graphLinks.js
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 17:31:30 +0000 (17:31 +0000)]
Code of metadataLib.xsl to share with makeGraphLinks.xsl extracted to
graphLinks.js
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 16:40:08 +0000 (16:40 +0000)]
Bug fixed: now links to metadata are created iff at least one pointer is there.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 16:15:41 +0000 (16:15 +0000)]
metadataControl and demultiplexMutual merged together into metadataControl
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:59:16 +0000 (15:59 +0000)]
metadataLib2.xsl renamed makeGraphLinks.xsl and committed.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:58:16 +0000 (15:58 +0000)]
Stylesheet to add links menus to graphs added.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:33:16 +0000 (15:33 +0000)]
New procedure to create metadata committed and old procedure removed.
The new procedure is based on ocaml code and builds metadata for both
forward and backward pointers. The old one was based on a stylesheet.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:15:19 +0000 (15:15 +0000)]
mk_meta_graph.xsl and mk_dep_graph.xsl factorised using
mk_meta_and_dep_graph.xsl.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 14:14:14 +0000 (14:14 +0000)]
mk_dep_graph reimplemented using the forward-pointers metadata.
It is now almost a perfect copy of mk_meta_graph.xsl.
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.