"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

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)

Added URL quoting to quote also "," (required by Netscape for plug-outs)

Initial revision

contentlib.xsl improved, now handles eq eqT

Bug nat_double_ind solved.

Bug fixed: the result was declared as gzipped even when it was not so

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

pure ==> proof_transform for the "by" part of rewriting

pure ==> noannot in CASE's branches

Big bug: & was not quoted in the URL for xmluri (that actually always had
one)

fonts for lambda prod and forall enlarged

characters in symbol font unified in size

abstract polinomials

added notations for abstact polinomials
HTML rendering of constants in symbol font improved (including m:minus)
added a title for the HTML rendering window

added support for HELM_GETTER_URL environment variable

first steps towards new interface with UWOBo and new stylesheets

added gmon.out

*** empty log message ***

Line morally belonging to lablgtk/*.h now is there! Hence, removed

Complete management of inductive types.
or_ind revisited (full_or_in).
(only for html: mml_extension must be upadated!!!).

-- andrea

Updated to lablgtk 1.2 and ocaml-3.01.

Modified Files:
1) mmlextension.xsl: added import of mmltheoryextension.xsl
2) objcontent.xsl: added *[1] to apply-templates
Added Files:
1) mmltheoryextension.xsl: MML presentation of objects in theories

Now links are followed even in theory + MathML Presentation

headercontent.xsl added to have all the notational stylesheets included in
the same place

patched_dtd => patch_dtd

more notations added

- added support for file ls (i.e. you can use a baseuri that point to a
  file with ls)
- change the installcgi method in Makefile, now no error if no cgi is
  going to be installed

basic notations for arithmetics

added notation for arithmetics

Changes in raw mode interface

Now uses the new stylesheets waterfall

error: "iso8859-1" ==> "'iso8859-1'"

makeURL() and related variables and parameters moved to links_library.xsl
prop.* now passed on as param.*

Modified Files:
1) expandobj.xsl, link.xsl: changed param media-type

Modified Files:
1) theory_pres.xsl: syntax error

Modified Files:
1) content_to_html.xsl, expandobj.xsl, html_init.xsl, html_reals.xsl,
html_set.xsl, theory_pres.xsl: now links are uri
Added Files:
1) link.xsl: transformation of uri into url

Modified Files:
1) theoryobject.dtd: added theory structure

getciconly ==> getxml

Modified Files:
1) expandobj.xsl, params.xsl, theory_content.xsl, theory_pres.xsl: new structurefor theories
2) params.xsl: adding mode="pure" in abstparams
Added Files:
1) objtheorycontent.xsl: new content generation for objects in theories

Added support for CGI handling, still remain some problems for headers,
but it works !
- Makefile.in:
  - added some targets like: install and uninstall for getter and cgi
- configure.in
  - added variable substitution for @HELM_CGI_DIR@
- http_getter.pl.in
  - added subroutine html_nice_answer (wrapper for simple html answers)
  - CGI handling when request ends with ".cgi"

getciconly ==> getxml

- renamed /getciconly in /getxml
- added control on not existent url
- added /resolve method

Annotations now working again (even if in a bit trickier way).
The get method of the getter could now be safely removed... URRAH!

Changed default content type from "text/plain" to "text/xml".

Various changes:
- added "patch_dtd" parameter to /getciconly method
- removed "remove_header" feature to the download subroutine
- patched response in gz file answering (now use x-gzip encoding header)
- remove /conf method
- removed hard coded "localhost" url

Raw mode now really considers compressed/not compressed

Added "format" support to /getciconly method.
Format may be one of "gz" or "normal", it sets the format of the returned
file either gzipped or uncompressed data.
"format" parameter may also be omitted.

Method get of the getter no more used. Replaced by getciconly
(whose name is now insignificant)

ehm ... no comment

Fixed a bug in the case cachemode=gzipped, resourcetype=normal.
(note: it's time to adopt "use strict" in http_getter.pl !!!!)

Files with annotations available now use a different icon

Used for files where annotations are availables

annotations now taken in account (as was for naturalLanguage)