new universes implementation

Ordering is now done in no-case style.

theory:path/index.theory are not rewritten to theory:/path.theory
if theory:path/index.theory exists in the database.

New filtering function for "Auto" tactic using "just costraints"

Back compatibility code introduced:
 1. the ls method maps a theory theory:/path/filename.theory
    to theory:/path/filename/index.theory iff there exists at least
    one object of the form cic:/path/filename/*
 2. the getter handles every URI theory:/path/filename/index.theory as
    the normalized URI theory:/path/filename.theory

The theory index.theory, if present, is shown at the beginning of the
listing.

* makeProofTreeURL ported to the new interface

.body removed from bread crumb trail

Links in the control frame when the URI ends with .body are now handled
correctly (i.e. the .body is removed if meaningless, as for the proof-checker
or the metadata).

<xsl:import href="toplevel_header.xsl"/>
moved here from show_dc.xsl

<h1> ==> <h3>

stylesheet L added to the metadata chain

bread crumb trail added

metadataLib.xsl merged into metadataControl.xsl

Dead code removed.

defaults.js no longer in use

Files control.js graphLinks.js utils.js no longer in use.

Dead code inclusion removed.

No longer in use.

No longer in use.

ls2html.xsl no longer in use

Form to choose the number of nodes to show removed ;-(

&2C ==> %2C

Dead code removed.

New HELM interface almost stable.

* it is now possible to set multiple parameters upon creation (or cloning)
  of a new profile

* setpassword passwords swapped

* implemented setparams method for setting multiple parameters at once

...

param.processorURL added (need by the search engine)

target="_top" added to Search.

Link to the search-engine hard-coded.

Major interface upgrade still going on. But we are approaching the end of the
tunnel.

New icons.

Major interface upgrade still going on. But we are approaching the end of
the tunnel.

Bug fixed: ls?baseuri=(cic|theory):/a/ also returned theory:/a.theory.

* getparams returns annotated pairs key,values

bugfix in /ls: removed double trailing "/"

ported to regexp based /ls method

changed /ls method so that regular expressions are used instead of plain
URIs

Major interface improvements.

* bumped to new version

* added external documentation in tex format
* true=>public and false=>private for permissions

JSMmenu links fixed.

###############################################################
### Partial major upgrade of the HELM/MoWGLI Web interface. ###
###############################################################

WARNING: requires the new UWOBO profiles.

Known bugs:

 1. the JSMmenu for graphs is broken
 2. the configuration stuff is utterly broken: you should rely on
    the default configuration
 3. only HTML has been tested (MathML and ProofTrees are broken for
    sure)
 4. dead code everywhere (e.g. almost all the existent
    javascript code; several tokens in links_library.xsl)

New: UWOBO profiles added.

written a new sort function to postpone the resolution of some types of the goals

don't remove documentation on "make dist" so that documentation will be
part of the generated tarball

* setprofileparam ==> setparam
* serialization/deserialization of the profile file implemented (write-through
  semantics)
* cloning of a profile fixed

added hostname resolution entry

implemented hostname resolution for "addr" parameter

rewritten "start" comment, now is almost decent

emptied implementing all items

removed spurious messages

- ported to latest API
- bumped copyright info

- added basic_auth.ml example
- restyled examples list

debian snapshot (towards a release)

added OO interface

* preliminary version of profile management

* updated respond_error messages after API change in ocaml-http 0.0.9

Added a sort function to decide the order of theorems to try in the tactic "auto".

added file locking while writing configuration to file (save_to)

open Helm_registry per default

bumped copyright years

Changed mapping keys <-> environment variables, mixed case envvars are
now used.

ported to latest ocaml-http API

ported to latest ocaml-http API

reverted code parameter on respond function to its original optionality

rebuilt

ported to latest ocaml-http API

written entry for 0.0.9

restyled API so that respond_* are statically typechecked

- changed API so that respond_* are statically type checked for correct
  parameter instantiation
- restyled a lot of code

added support for HEAD requests

http basic authentication example

added support for HTTP (Basic) authentication

- added support for HTTP (Basic) authentication
- simplified usage of some internal optional parameters

* hbugs moved in ocaml

added some nested sections in order to test "ls" method

- added "has" method
- added "ls" method
- added "?prefix" parameter to "fold", "iter" and "to_list" methods

added helm-pxp, now needed

expanded content of old topfind

no longer needed

added iterators over registry contents (fold, iter, to_list)

Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

Bug fixed: middle-clicking over links in the listing frames should now
work on any browser.

Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

first moogle template checkin

* the input of the function mkMetaTheoryURL must an (unquoted) URI. Fixed.

* the URI passed to the rdfly deamon is now CICURI, except that quoting
  rules are different.

* [Luca] string concatenation now made using String.concat instead of
  List.fold_left

Nuova implementazione di Auto "breadth-first".

xml:base and helm:base are now generated only for theories.

* tactics/Makefile fixed (to remove duplicate .mli files)
* .depend regenerated

Bug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
were full URIs (with also the filename at the end). Fixed by using
Filename.dirname (that seems to work also with generic URIs).

Added a filter for uris in tactic "auto".
Uris of theorems containing, in the conclusion or in the hypothesis, constants not present in the proof (hypothesis or conclusion) are filtered out.

Added support for xml base(s) URL and URI. The getter now adds these two
attributes (hopefully) on the first open tag

first check in of statefulProofEngine

bugfix: remove trailing slashes from dtd_base_urls

- some code patched
- mathql documentation updated