moogle snapshot

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

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

added .mli

got rid of a ~status label

got rid of ~status label

got rid of ~status label so that tactics can now be applied partially,
delta reduced, ...

added ocamlfind library checks to configure.ac

renamed mathita to matita

snapshot

ignore Makefile since now it's generated by configure

added Makefile.in

reorganized metas so that pxp is references only through helm-pxp

added hbugs' (client) meta

generalized META.* ignoring

- reordered modules so that pxp could be used as entry point for pxp
- added hbugs
- pretty printed modules

- use PxpHelmConf
- no longer use deprecated Pxp_yacc module

- use PxpHelmConf
- no longer use deprecated Pxp_yacc

use PxpHelmConf

added dep on Helm_registry

use PxpHelmConf module

- use PxpHelmConf
- removed references to deprecated Pxp_yacc module

- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
  belongs to Getter module!)
- added PxpHelmConf module, repository of Pxp configurations for helm

added ExtThread module, ex Hbugs_deity (a Thread module with killing
capabilities)

injected hbugs under ocaml/ dir

moved hbugs under ocaml/

fixed a typo (inside a comment)

test_equality_only was not used in sort comparison.
It should be implemented only in unification.

use respawner

changed logging message

removed deprecated uwobo_forever.sh

removed tedious "_mowgli" postfix

use new daemon_respawner.sh

fixed some typos in sample init.d

added generic daemon respawner

script deprecated

added newline to log when log_file is in use

- addead autoconf-iguration. Actually it only set the default runtime
  configuration file

- use new logger interface
- added support for log_level and log_file in configuration file

- rewritten http_getter logger interface

- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)

Metasenv added as parameter to eta_fixing.

s/dtd_base_url/dtd_base_urls/

- better pretty printing of exceptions (added red color)
- added "-update" command line parameter for batch updating

- fixed dtd_base_urls implementation
- factorized a lot of code in document patching