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)

First version of metadata interface.
Still many things to be fixed and one stylesheet (of Andrea) not committed.
But it is a new beginning...

Repository created.

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

# bugfix: rdf tie that proxies rdf_urls_of_uris.db now works even after
  invocation of /update method

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!

Format of rdf URIs relaxed

Version modified

Now helm:rdf:... is a valid URI.
Before it had to be helm:rdf/:...

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

UNICODEvsSYMBOL introduced everywhere. (work completed)

UNICODEvsSYMBOL introduced

Bug fixed: Compressed was not checked well on control frame load.
"yes" ==> "compressed"

Comment removed because XSLT removed the "end-of-line" after it, making it
extends too much, commenting out the following lines. ;-(

"Bug" appearing under IE only fixed.

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.

resolve_topurl.xsl added

Some simplifications (redundant code).

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"

UNICODEvsSYMBOL parameter now added everywhere

Small bugs fixed:

 mathcolor ==> color in <FONT>
 arrow size set equal to "+0"

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.

drop_coercions added

BUG LAMBDA fixed.

drop_coercions.xsl has been added

Default for patch_dtd modified to "yes".

xsl:import to cope with new xalan version

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

Aggiunto lambda.xsl

Lambda notazione.

Modified Files:
1) maththeory.dtd, theoryobject.dtd: new structure for xml and content theories

URI may now have #

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?)

Attribute @name of ENTITY removed.

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

Relative anchors (#xxx) should be followed _inside_ the current document.

minidom.c : fixed memory leak

New standard stylesheet genmmlid.xsl added.

New version of Igor Rodionov stylesheets.

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

':' 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?)

Stylesheets for (cic|content|presentation) theory now fully working

Bug fixed: following a link to an object inside a theory opened the
 object with the header of the theories.

Bug fixed: following a link to an object inside a theory opened the object
 with the header of the theories.

Links not starting with cic: or theory: are now left untouched and
open a new _blank window

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

.cvsignore files missing

Initial revision

register method added

annotationHelper now working again. A control frame has been added to
the CIC or the Theory window to invoke the annotationHelper.

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.

Initial revision

Some adjustments in the licenses

Modified Files:
  acconfig.h main.c

Initial revision

panel ==> uwobo-panel

Content-Cache, Expires and Pragma added for non-error responses.
Should them be there also in case of errors?

Control frame added to CIC window

In natural language, non vengono piu' stampati glia argomenti
delle applicazioni con sort divers da prop.

Control panel added to CIC window

Unstable commit: just before removing next/prev functionalities

Modified Files:
1) arith.xsl, contentlib.xsl, reals.xsl, ring.xsl: removed xlink declaration