This commit was manufactured by cvs2svn to create tag 'premoogle'.

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

changed proofStatus so that uri component is optional (useful to start an
unnamed proof or leave the possibility of postpone uri choice)

*** empty log message ***

Adding file newConstraint
The file contains functions for computing prefixes and related
stuff, required by the new management of matching.

Adding file match_concl
the file contains:
   - functions executing must, just and only constraints on the mysql
     data base;
   - the general function cmatch for retrieving all statements matching
     a given conclusion

snapshot (notably: first working version of the console)

- moved up in the grammar precedences command entry so that sequence of
  commands are not permitted
- added parsing of "abort" command

removed traliling dot in command pretty printer, now it's added by the
tactical pp

added Abort and Check commands

embedded commands ast into tacticals ast

- moved command as sub-entries of tactical grammars (as per tactics)

snapshot

- moved applyTransformation initialization code to the relevant library
- decoupled termViewer from ChosenTransformer

moved here initialization code (previously in gTopLevel/termViewer.ml)

snapshot

- added a configuration variable for selecting between fresh instances
  for numbers or not (set by default to a single instance)

snapshot

added a TODO comment

rebuilt

added extra "id" parameter for input_or_locate_uri callback

- split logic operators away from aritmetic ones so that
   \forall n:nat. n > 0 \or n = 0
  is parsed "correctly"

removed file:// prefix from local_library key, hopefully it isn't useful

snapshot

gt URL pointed to lt

Universes introduction

rdfly hardcoded URL changed from mowgli.cs.unibo.it to localhost

expandasking parameter passed to UWOBO.

snapshot

mysql_connection.* keys added

mathql_interpreter.mysql_connection.* keys added.

added (and used) some type shorthands

- added some type shorthands
- added license information

rebuit

Patches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
It is interesting to understand whether it is still necessary (after
the CicUnification bug fix) or not.

Big bug fixed: in the case  t <?= ?1, the instantiation ?1 := t was generated
and then t : C and ?1 : E were retrieved/computed correctly; then
E <?= T was incorrectly tested (instead of T <?= E).

fourier.mli addedto interface files.

snapshot

added /help method (needed by respawner)

IMPLEMENTATION_FILES now generated from INTERFACE_FILES.

added .cvsignore

detects and uses {ocamlc,ocamlopt}.opt when available

detect and use {ocamlc,ocamlopt}.opt when they are available

exported term_of_uri

added helmLibraryObjects.mli mention