New copyright free implementation of menus in JavaScript.

BUG Fixed: arcs with attributes were not processed in the right way.

Some comments added.

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...

Small bug: the theory was open in the graph windows instead of its own.

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.

There were still many problems with URIs with a ' in the middle.
Now they should be all resolved (in theory, at least ;-)

Also starting from metadatas it is now possible to select the number
of nodes.

Clicking on the AREA and not on the menu just pop-ups the menu again instead
of crashing.

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 ;-)]

A -> B now means "A depends on B" both in backward and forward graphs

A link to the theory of backward dependencies added to the menu.

The code to create a link to the theory automatically generated from the
backward metadata has been moved here from metadataLib.xsl.

Code clean-up: the code to create the link to the theory automatically
generated from the backward metadata has been moved to makeGraphLinks.js

The JavaScript code is now defined in on-line/javascript/graphLinks.xsl and
it is shared with medataLib.xsl.

Code obtained from the factorization of makeGraphLinks.xsl and metadataLib.xsl

Oooops. I have exchanged the targets of the links to the graphs of
forward and backward dependencies. Fixed.

Code to share with makeGraphLinks.xsl extracted to graphLinks.js

Code of metadataLib.xsl to share with makeGraphLinks.xsl extracted to
graphLinks.js

Bug fixed: now links to metadata are created iff at least one pointer is there.

metadataControl and demultiplexMutual merged together into metadataControl

metadataLib2.xsl renamed makeGraphLinks.xsl and committed.

Stylesheet to add links menus to graphs added.

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.

mk_meta_graph.xsl and mk_dep_graph.xsl factorised using
mk_meta_and_dep_graph.xsl.

mk_dep_graph reimplemented using the forward-pointers metadata.
It is now almost a perfect copy of mk_meta_graph.xsl.

RDFURI removed because no more unique.

Ported to RDF syntax.

Porting to RDF syntax.

The cache now supports different RDF URI schema at the same time.

template mk-mml-op-noannot was modified to allow hidden parameters
eq and eqT where aligned

Initial revision

Bug fixing: now the link to the graphs produce extended URIs
(e.g. ".../nat.ind#xpointer(1/1/1")

mk_dep_graph.xsl now differentiates the constructors from the
inductive types producing "extended" URIs
(e.g. ".../nat.ind#xpointer(1/1/1)")

Oooops. After the last commit all the URLs were damaged.

Makefile.in that support some new architectures.

Bug removed/Feature changed: CIC URIs for inductive data types
and constructors ending with an #xpointer are now handled
(more) correctly.

Bug related to #xpointer(1/n/m) constructor URI fixed.

New implementation of the graph stuff: now every hard-coded URL has been
removed.

Help method added

New implementation of the graphs stuff: now every hard-coded URL has
been removed.

Commented code removed

New implementation of the graph staff: the logic has been moved
from mk_html.pl to the stylesheets

New implementation of the graph staff: logic moved
from mk_html.pl to the stylesheets.

Whoops. Forgot to open the CIC file in the cic window.

Menu in JavaScript substituted to multi-area links. Cool.

Code improvement, same functionalities.

New implementation: now the number of nodes is used to prune the graph

cvsignore added

First release checked in

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.

Debian packaging of helmpot-0.0.3

Many more hard-coded links removed.

First set of hard-coded URLs removed.
Still many remaining.

Absolute path removed thanks to a bug-fixing in Uwobo.
To process this stylesheet, a version of Uwobo >= 1.1.11 is required.

First implementation of graphs stuff. Working on my notebook,
probably not working on-line, yet.

New stylesheets for graphs added

d_c missing

First implementation of graphs. Working on my notebook, probably not
on-line.

* 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.

bug fix (helm selection) and new version (sigh)

Proof explosion blocked after lambda-abstractions.

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)

1. Fixati alcuni problemi di indentazione con le rewrite.
2. Esplosione in un colpo solo di catene di riscrittura.

Espansione dinamica delle prove per Mozilla/Galeon.

Upgrade to 0.0.2

* Title added
* Method onLoad="window.focus()" added. To be removed as soon as the window
  become a frame.

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.

configure.in : new version

Modified Files:
1) mmlextension.xsl: m:xref fixed

----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: m:xref fixed
----------------------------------------------------------------------

----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: added notation for lambda calculus
----------------------------------------------------------------------

----------------------------------------------------------------------
Modified Files:
1) content_to_html.xsl html_init.xsl html_reals.xsl html_set.xsl: added
control on the existence of definitionURL
----------------------------------------------------------------------

Bug in zarith notation corrected.

----------------------------------------------------------------------
Modified Files:
1) content_to_html.xsl: bug fixed
----------------------------------------------------------------------

----------------------------------------------------------------------
Modified Files:
1) content.xsl content_to_html.xsl mmlextension.xsl: added MML
piecewise for Mutcase patterns
----------------------------------------------------------------------

"Recursive" notation for Z.

----------------------------------------------------------------------
Modified Files:
1) mmlctop.xsl-0.14, mmlextension.xsl: changed mchar into entities and
formatted new proof elements.
----------------------------------------------------------------------

Fixed a problem of Netscape with 'file:///' URL.
Now the stylesheets are copied inside every HTML file instead of
creating a <link/> to them.

First version using maction/toggle to navigate proofs.

Added explodeall parameter (default="false") to generate mactions with
only the exploded component. Used during annotation.

Metadata were broken in MathML presentation mode.

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

added preliminary support for maction
- cursor bug

Two parameters used but not declared. Fixed.

Notation for ZArith (inside arith.xsl) added.

drop_coercion (d_c) inserted in every stylesheet chain

mk_meta_theory.xsl added

Makefile fixed (too many parameters on command line);
xslt/occurrences.xsl added

topurl parameter now passed around

First completely working interface for metadata.

":" bug in theory_pres fixed.

small error inside mk_meta_theory.

mk_meta_theory.xsl added
It generates a theory starting from metadata.

occurrences.xsl added
It computes all occurrences of identifiers inside a given document.
It is used for computing metadata.

ht:OBJECT added;
ls.dtd added

ht:OBJECT added

Total compatibility with Mozilla 9.1 reached with this commit.

.cvsignore added

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)