- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel

make and clean also in html/

removed old HTML files (tagged with "old_htmls")

moogle.html is now generated, it do not needs to be in CVS

generate HTML templates using XSLT starting from a bunch of .src files

look and feel improvements

- re-enginered main moogle template, it is now aware of queries kind, summary,
  and results. This enable fixing of minor like feedback on the query kind in
  case of errors
- minor bug fixes: 1/0 nuisance in case of errors
- commented out advanced query selection (which do nothing)

- handle metavariables: if at least one of them is present, then the
  cardinality constraint is not enforce
- commented out debugging prints

bugfix when user query contains metas: their context should not be analyzed
as it were in main position

Bugfix in restore_from_channel, before this fix hashtable (which has uris as
keys and pairs <objects,universe> as values) was dumped but restored as if it
have uris as keys and objects as values. That caused immediate segfaults
while trying to iterated on the restored table.

added support for open terms in check

support for terms with metas in check

added choose_uri method to console, used by the interpreter to implement the
hint command

Added heuristic in the Appl case, we beta-expand only if the argument list
does't contain metas.

Fixed remove operation and get_obj (that now correctly searches in the
unchecked_list).

moved a debug print so that it is executed for each phrase

adapted to optional comment lexer interface

renaming "remove_term" -> "remove_obj"

- fix in intro parsing
- avoid generating seq tactical for a 1-length sequences

factorized tacticals separator and terminator

added "unindex" to undo indexing of a single object

bugfix: method 'advance' now took in input concrete syntax since atm
pretty printing is not the inverse operation of parsing

changed toolbar window type

bugfix: avoid executing tactic for the script twice

removed spurious dependency on Dbi_mysql

added script support a la coqide

- fixed "error loading dom error" avoiding sequent_viewer be delivered
  the destroy signal when resetting the notebook
- added singleton instances of sequent_viewer and sequents_viewer

moved lockScript to MatitaScript module

0.1.0-1 entry

strip debian version from META version

use wildcard in install target so that binary objects are installed only
when built

added a missing unchecked_to_frozen (fixes a Not_found exception while
type checking without trust)

at_least now supports the ownerized tables

added boxml namespace

- changed license to lgpl
- bumped copyright
- improved ocamldoc comments

debian changes target release 0.1.0

included lgpl

added TODO file

added support for directory browsing in cicBrowser

rebuilt

connected change tactic (proof of concept)

removed chosenTransformer.ml*

removed chosenTransformer.mli

sync with Xml.pp

fix join on multiple tables

fixed Gzip bug in Xml.pp

saves to gzip

added library table and owner tables handling in the SQL code

escape exception name and arguments embedded in root element attributes
to avoid non well formed xml documents to be generated

bugfix: handling of local resources (not to be cached) when they are zipped,
avoid former Sys_error exception for not existent files

changed local_url so that it returns the local part of a file:// scheme url

- removed special handling of universes (no longer needed)
- removed ancient part of commented code

"thin" version of the configuration file (exploits default values and
new configuration parameters like maps_dir and cache_dir)

- added some default values (no longer explicitely required in the
  configuration file)
- bugfix: read configuration values from the environment and not
  directly via Helm_registry

added gzip support to Xml

locate now searched bot the standard library and the owner(user) library

fix

return also .types uri in getalluris/

snapshot, notably:
- even more singleton instances: disambiguator is now common to matita
  and matitac, but matita set different callbacks which uses gtk
- getter now embedded in matita (no longer use remote getter)
- use onwerization of tables

parameterized lexer so that comment tokens could be returned or not,
per default they are not returned

removed dep on mathql

rebuilt

- removed dependency on mathql
- cosmetic changes

- added init method
- added default values for loglevel and logfile

rebuild

- simplified environment handling:
  * added a lot of default values
  * use maps_dir instead of dbm files file-per-file
  * use cache_dir instead of cache dirs dir-per-dir
  * servers could now either be listed in servers.txt or directly in
    configuration file

local_url predicate (recognize file:// urls)

do not cache local resources (i.e. file:// urls)

create path towards dbm file

removed ancient mathql deps

- clean no longer unregister URIs from the getter, but returns them
- removed owner table handling

cosmetic changes

target 0.1.0 changelog (not yet released ...)

uniformed default values handling, now they are all in this module and
consistent with optional arguments of start functions

- added main that starts a new http_daemon given a daemon_spec (see
  Http_types.daemon_spec)
- added default_spec
- deprecated start and start' in favour of main

cosmetic changes (no longer open Neturl)

removed Makefile.overrides

rebuilt

- moved ocamldoc comments in .mli
- added daemon_spec

added warn and error for messaging

added http_types.mli: Makefile.overrides is now useless

removed useless dont_fork and obj_foo examples

ported to daemon_spec

- ported to daemon_spec
- used as example of exn_handler to avoid sigpipe kill processes
  holding mutexes

- added sigpipe handling to avoid processes get killed by unhandled
  SIGPIPE
- cosmetic changes

added head_callback to access response status and headers in requests

fixed currentproof

better owner hadling
better basedir non existent path handling
matitaDb module to set up and clean owner metadata environment

MetadataDb.clean doesn't need ~owner since table names are ownerized ;)

owners table not needed

added new ownerize function

new metadataTypes interface (with ownerize function)

removed uri parameter from load_proof

rebuilt

snapshot, notably:
- refactoring of modules and classes: added a lot more of constructors
  and singleton instances so that objects that are really singleton
  (e.g. disambiguator, parser, db handle, ...) are not passed between
  functions
  Note that objects that are dependent on whether we are running matita
  or matitac (like the console) can't be made singleton

removed spurious load of a local gTopLevel.conf.xml

- implemented inductive type rendering
- added hyperlinks on parameters

added inductive_name field to inductive definitions so that this
information is not lost at content level

added (linked to matita) executable cicbrowser: when invoked it only shows
a cicBrowser window which can be used to browse the library

snapshot, notably:
- removed check window and proof window
- implemented cicBrowser which can be used to render current proof,
  term the user wants to check and any other object from the library
  using a www-browser-like interface