This commit was manufactured by cvs2svn to create branch 'xmltheory'.

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)

Fixed bug in .ann extension handling.

Syntax error + new indenting

Configuration on-line now pass the parameters

Initial revision

Last update before dismission

Added dtd reference in ls method while generating xml output.

Modified Files:
1) expandobj.xsl: comments
2) objcontent.xsl, params.xsl: parameters abstraction from objcontent to params

Modified Files:
1) content_to_html.xsl: removed mtext, modified output and added
naturalLanguage
2) theory_content.xsl: generate only content markup for theories
3) theory_pres.xsl: generate only html pres for theories, starting
from the corresponding content markup
Added Files:
1) expandobj.xsl: expand objects generating the corresponding content
markup or the pres one, starting from the markup for theories

the version command has been renamed into help, the syntax of the available
commands will be added soon

processorURL must now already end with a /

Now the on-line interface can use a Getter and an UWOBO on any machine

Bug fixed: now propagates informations about inner-types usage and
natural language when following hyperlinks.

WARNING: to create an hyperlink, it is no more enough to concatenate
 $header and the URI. You need to call the new makeURL() named-template.

*** empty log message ***

getter flags considered

Added ordering in ann and types flags

library3 ==> javascript

New on-line interface

New online interface

The .types files are now read directly by the stylesheets.
Two new params added: naturalLanguage and CICURI

Now uses the param keys

new version of ls,
now meet the specifications ?????

added eq_ind

Fixed a bug in CGI creation, method "update" now work ! :)

patch for libxml2 new release

WebEQ definitely no more used

Changed syntax for 'ls' method:
  wget http....localhost:8081/ls?baseuri=<uri>&format=[txt|xml]
Now is possibile to:
 - use ls for 'cic:' uris
 - use ls for 'theory:' uris
 - coming soon support for 'any' uris
Now getter use CGI module, added this dep. to configure.in

commented processing instructions for Cocoon, we do not use it any more

now do unescaping of incoming URI

added the patch on-the-fly for DTDs, fixed the script for launching the getter at boot time

New stylesheets from content to html.

-- andrea

Added 'ls' method: return a list of uri that begin with a given uri.
Response may be in CR-separated line or in a simple XML document.

helm_wget subroutine now use LWP module and doesn't use any more external
wget program