]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agofix join on multiple tables
Stefano Zacchiroli [Fri, 4 Feb 2005 16:52:29 +0000 (16:52 +0000)]
fix join on multiple tables

20 years agofixed Gzip bug in Xml.pp
Enrico Tassi [Fri, 4 Feb 2005 16:15:44 +0000 (16:15 +0000)]
fixed Gzip bug in Xml.pp

20 years agosaves to gzip
Enrico Tassi [Fri, 4 Feb 2005 16:13:28 +0000 (16:13 +0000)]
saves to gzip

20 years agoadded library table and owner tables handling in the SQL code
Enrico Tassi [Fri, 4 Feb 2005 15:47:40 +0000 (15:47 +0000)]
added library table and owner tables handling in the SQL code

20 years agoescape exception name and arguments embedded in root element attributes
Stefano Zacchiroli [Fri, 4 Feb 2005 15:04:53 +0000 (15:04 +0000)]
escape exception name and arguments embedded in root element attributes
to avoid non well formed xml documents to be generated

20 years agobugfix: handling of local resources (not to be cached) when they are zipped,
Stefano Zacchiroli [Fri, 4 Feb 2005 15:03:58 +0000 (15:03 +0000)]
bugfix: handling of local resources (not to be cached) when they are zipped,
avoid former Sys_error exception for not existent files

20 years agochanged local_url so that it returns the local part of a file:// scheme url
Stefano Zacchiroli [Fri, 4 Feb 2005 15:03:22 +0000 (15:03 +0000)]
changed local_url so that it returns the local part of a file:// scheme url

20 years ago- removed special handling of universes (no longer needed)
Stefano Zacchiroli [Fri, 4 Feb 2005 15:02:38 +0000 (15:02 +0000)]
- removed special handling of universes (no longer needed)
- removed ancient part of commented code

20 years ago"thin" version of the configuration file (exploits default values and
Stefano Zacchiroli [Fri, 4 Feb 2005 14:03:03 +0000 (14:03 +0000)]
"thin" version of the configuration file (exploits default values and
new configuration parameters like maps_dir and cache_dir)

20 years ago- added some default values (no longer explicitely required in the
Stefano Zacchiroli [Fri, 4 Feb 2005 14:02:20 +0000 (14:02 +0000)]
- 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

20 years agoadded gzip support to Xml
Stefano Zacchiroli [Fri, 4 Feb 2005 13:58:53 +0000 (13:58 +0000)]
added gzip support to Xml

20 years agolocate now searched bot the standard library and the owner(user) library
Enrico Tassi [Fri, 4 Feb 2005 13:02:57 +0000 (13:02 +0000)]
locate now searched bot the standard library and the owner(user) library

20 years agofix
Enrico Tassi [Fri, 4 Feb 2005 13:01:29 +0000 (13:01 +0000)]
fix

20 years agoreturn also .types uri in getalluris/
Stefano Zacchiroli [Fri, 4 Feb 2005 12:11:07 +0000 (12:11 +0000)]
return also .types uri in getalluris/

20 years agosnapshot, notably:
Stefano Zacchiroli [Fri, 4 Feb 2005 11:10:52 +0000 (11:10 +0000)]
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

20 years agoparameterized lexer so that comment tokens could be returned or not,
Stefano Zacchiroli [Fri, 4 Feb 2005 09:30:47 +0000 (09:30 +0000)]
parameterized lexer so that comment tokens could be returned or not,
per default they are not returned

20 years agoremoved dep on mathql
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:50 +0000 (09:29 +0000)]
removed dep on mathql

20 years agorebuilt
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:03 +0000 (09:29 +0000)]
rebuilt

20 years ago- removed dependency on mathql
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:42 +0000 (09:28 +0000)]
- removed dependency on mathql
- cosmetic changes

20 years ago- added init method
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:07 +0000 (09:28 +0000)]
- added init method
- added default values for loglevel and logfile

20 years agorebuild
Stefano Zacchiroli [Fri, 4 Feb 2005 09:27:30 +0000 (09:27 +0000)]
rebuild

20 years ago- simplified environment handling:
Stefano Zacchiroli [Fri, 4 Feb 2005 09:26:59 +0000 (09:26 +0000)]
- 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

20 years agolocal_url predicate (recognize file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:46 +0000 (09:24 +0000)]
local_url predicate (recognize file:// urls)

20 years agodo not cache local resources (i.e. file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:01 +0000 (09:24 +0000)]
do not cache local resources (i.e. file:// urls)

20 years agocreate path towards dbm file
Stefano Zacchiroli [Fri, 4 Feb 2005 09:23:27 +0000 (09:23 +0000)]
create path towards dbm file

20 years agoremoved ancient mathql deps
Stefano Zacchiroli [Fri, 4 Feb 2005 09:15:40 +0000 (09:15 +0000)]
removed ancient mathql deps

20 years ago- clean no longer unregister URIs from the getter, but returns them
Stefano Zacchiroli [Fri, 4 Feb 2005 09:15:10 +0000 (09:15 +0000)]
- clean no longer unregister URIs from the getter, but returns them
- removed owner table handling

20 years agocosmetic changes
Stefano Zacchiroli [Fri, 4 Feb 2005 09:14:32 +0000 (09:14 +0000)]
cosmetic changes

20 years agotarget 0.1.0 changelog (not yet released ...)
Stefano Zacchiroli [Thu, 3 Feb 2005 22:31:35 +0000 (22:31 +0000)]
target 0.1.0 changelog (not yet released ...)

20 years agouniformed default values handling, now they are all in this module and
Stefano Zacchiroli [Thu, 3 Feb 2005 22:25:16 +0000 (22:25 +0000)]
uniformed default values handling, now they are all in this module and
consistent with optional arguments of start functions

20 years ago- added main that starts a new http_daemon given a daemon_spec (see
Stefano Zacchiroli [Thu, 3 Feb 2005 22:24:29 +0000 (22:24 +0000)]
- 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

20 years agocosmetic changes (no longer open Neturl)
Stefano Zacchiroli [Thu, 3 Feb 2005 22:20:29 +0000 (22:20 +0000)]
cosmetic changes (no longer open Neturl)

20 years agoremoved Makefile.overrides
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:48 +0000 (22:19 +0000)]
removed Makefile.overrides

20 years agorebuilt
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:13 +0000 (22:19 +0000)]
rebuilt

20 years ago- moved ocamldoc comments in .mli
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:00 +0000 (22:19 +0000)]
- moved ocamldoc comments in .mli
- added daemon_spec

20 years agoadded warn and error for messaging
Stefano Zacchiroli [Thu, 3 Feb 2005 22:18:26 +0000 (22:18 +0000)]
added warn and error for messaging

20 years agoadded http_types.mli: Makefile.overrides is now useless
Stefano Zacchiroli [Thu, 3 Feb 2005 22:17:54 +0000 (22:17 +0000)]
added http_types.mli: Makefile.overrides is now useless

20 years agoremoved useless dont_fork and obj_foo examples
Stefano Zacchiroli [Thu, 3 Feb 2005 22:12:53 +0000 (22:12 +0000)]
removed useless dont_fork and obj_foo examples

20 years agoported to daemon_spec
Stefano Zacchiroli [Thu, 3 Feb 2005 22:12:18 +0000 (22:12 +0000)]
ported to daemon_spec

20 years ago- ported to daemon_spec
Stefano Zacchiroli [Thu, 3 Feb 2005 22:11:55 +0000 (22:11 +0000)]
- ported to daemon_spec
- used as example of exn_handler to avoid sigpipe kill processes
  holding mutexes

20 years ago- added sigpipe handling to avoid processes get killed by unhandled
Stefano Zacchiroli [Thu, 3 Feb 2005 22:10:46 +0000 (22:10 +0000)]
- added sigpipe handling to avoid processes get killed by unhandled
  SIGPIPE
- cosmetic changes

20 years agoadded head_callback to access response status and headers in requests
Stefano Zacchiroli [Thu, 3 Feb 2005 22:06:01 +0000 (22:06 +0000)]
added head_callback to access response status and headers in requests

20 years agofixed currentproof
Enrico Tassi [Thu, 3 Feb 2005 16:46:12 +0000 (16:46 +0000)]
fixed currentproof

20 years agobetter owner hadling
Enrico Tassi [Thu, 3 Feb 2005 16:45:22 +0000 (16:45 +0000)]
better owner hadling
better basedir non existent path handling
matitaDb module to set up and clean owner metadata environment

20 years agoMetadataDb.clean doesn't need ~owner since table names are ownerized ;)
Enrico Tassi [Thu, 3 Feb 2005 16:40:06 +0000 (16:40 +0000)]
MetadataDb.clean doesn't need ~owner since table names are ownerized ;)

20 years agoowners table not needed
Enrico Tassi [Thu, 3 Feb 2005 15:12:08 +0000 (15:12 +0000)]
owners table not needed

20 years agoadded new ownerize function
Enrico Tassi [Thu, 3 Feb 2005 14:32:22 +0000 (14:32 +0000)]
added new ownerize function

20 years agonew metadataTypes interface (with ownerize function)
Enrico Tassi [Thu, 3 Feb 2005 14:31:59 +0000 (14:31 +0000)]
new metadataTypes interface (with ownerize function)

20 years agoremoved uri parameter from load_proof
Enrico Tassi [Thu, 3 Feb 2005 13:14:04 +0000 (13:14 +0000)]
removed uri parameter from load_proof

20 years agorebuilt
Stefano Zacchiroli [Thu, 3 Feb 2005 10:43:22 +0000 (10:43 +0000)]
rebuilt

20 years agosnapshot, notably:
Stefano Zacchiroli [Thu, 3 Feb 2005 10:43:04 +0000 (10:43 +0000)]
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

20 years agoremoved spurious load of a local gTopLevel.conf.xml
Stefano Zacchiroli [Thu, 3 Feb 2005 10:40:49 +0000 (10:40 +0000)]
removed spurious load of a local gTopLevel.conf.xml

20 years ago- implemented inductive type rendering
Stefano Zacchiroli [Wed, 2 Feb 2005 14:12:24 +0000 (14:12 +0000)]
- implemented inductive type rendering
- added hyperlinks on parameters

20 years agoadded inductive_name field to inductive definitions so that this
Stefano Zacchiroli [Wed, 2 Feb 2005 14:11:41 +0000 (14:11 +0000)]
added inductive_name field to inductive definitions so that this
information is not lost at content level

20 years agoadded (linked to matita) executable cicbrowser: when invoked it only shows
Stefano Zacchiroli [Tue, 1 Feb 2005 18:24:28 +0000 (18:24 +0000)]
added (linked to matita) executable cicbrowser: when invoked it only shows
a cicBrowser window which can be used to browse the library

20 years agosnapshot, notably:
Stefano Zacchiroli [Tue, 1 Feb 2005 17:59:04 +0000 (17:59 +0000)]
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

20 years agoremoved useless parameter uri from mml_of_cic_object
Stefano Zacchiroli [Tue, 1 Feb 2005 17:56:54 +0000 (17:56 +0000)]
removed useless parameter uri from mml_of_cic_object

20 years agoadded mathml_ns
Stefano Zacchiroli [Tue, 1 Feb 2005 17:55:53 +0000 (17:55 +0000)]
added mathml_ns

20 years agoenriched error message
Stefano Zacchiroli [Tue, 1 Feb 2005 17:55:29 +0000 (17:55 +0000)]
enriched error message

20 years agoadded strip_xpointer: remove trailing #xpointer from a UriManager.uri value
Stefano Zacchiroli [Tue, 1 Feb 2005 17:54:49 +0000 (17:54 +0000)]
added strip_xpointer: remove trailing #xpointer from a UriManager.uri value

20 years agoreverder change. no more owner passed to the locate.
Enrico Tassi [Tue, 1 Feb 2005 15:40:15 +0000 (15:40 +0000)]
reverder change. no more owner passed to the locate.

20 years agoadded owner support to the disambiguator (now locate finds only objects
Enrico Tassi [Tue, 1 Feb 2005 15:21:20 +0000 (15:21 +0000)]
added owner support to the disambiguator (now locate finds only objects
of the current owner).

20 years ago*** empty log message ***
Enrico Tassi [Tue, 1 Feb 2005 13:47:00 +0000 (13:47 +0000)]
*** empty log message ***

20 years agoadded `Coer print_kind
Enrico Tassi [Tue, 1 Feb 2005 13:45:36 +0000 (13:45 +0000)]
added `Coer print_kind

20 years agoAdded Coer/Coercions print_kind
Enrico Tassi [Tue, 1 Feb 2005 13:45:05 +0000 (13:45 +0000)]
Added Coer/Coercions print_kind

20 years agoMetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
Enrico Tassi [Tue, 1 Feb 2005 13:44:27 +0000 (13:44 +0000)]
MetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
from the uris that deletes from the DB

20 years agofix in the coercions list generation and aded a function to know the
Enrico Tassi [Tue, 1 Feb 2005 13:42:35 +0000 (13:42 +0000)]
fix in the coercions list generation and aded a function to know the
known coercions

20 years agoadded the unregister method to the help page
Enrico Tassi [Tue, 1 Feb 2005 11:46:31 +0000 (11:46 +0000)]
added the unregister method to the help page

20 years agofixed coercions
Enrico Tassi [Tue, 1 Feb 2005 10:42:18 +0000 (10:42 +0000)]
fixed coercions

20 years agoremoved debug print
Enrico Tassi [Tue, 1 Feb 2005 10:05:52 +0000 (10:05 +0000)]
removed debug print

20 years agocosmetic fix to pp_location
Enrico Tassi [Tue, 1 Feb 2005 10:05:14 +0000 (10:05 +0000)]
cosmetic fix to pp_location

20 years agoadded save_object_to_disk and basedir
Enrico Tassi [Mon, 31 Jan 2005 17:29:03 +0000 (17:29 +0000)]
added save_object_to_disk and basedir

20 years agoadded delift
Enrico Tassi [Mon, 31 Jan 2005 17:18:55 +0000 (17:18 +0000)]
added delift

20 years agoadded basedir and improved let{rec} syntax
Enrico Tassi [Mon, 31 Jan 2005 17:17:32 +0000 (17:17 +0000)]
added basedir and improved let{rec} syntax

20 years agobetter debug prints
Enrico Tassi [Mon, 31 Jan 2005 17:16:41 +0000 (17:16 +0000)]
better debug prints

20 years agoadded Basedir Ast
Enrico Tassi [Mon, 31 Jan 2005 17:12:12 +0000 (17:12 +0000)]
added Basedir Ast

20 years agoAdded outtype inference to MutCase
Enrico Tassi [Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)]
Added outtype inference to MutCase

20 years agoFixed bug in delift. The recursive call in the Meta case was on t and not
Enrico Tassi [Mon, 31 Jan 2005 17:10:38 +0000 (17:10 +0000)]
Fixed bug in delift. The recursive call in the Meta case was on t and not
on t lifted to the meta local context.

20 years ago- removed applyStylesheets
Enrico Tassi [Tue, 25 Jan 2005 09:32:35 +0000 (09:32 +0000)]
- removed applyStylesheets
- added Print and print_kind to AST
- added coercion module

20 years agoadded list_obj and list_uri
Enrico Tassi [Tue, 25 Jan 2005 09:28:50 +0000 (09:28 +0000)]
added list_obj and list_uri

20 years ago- added code for Coercion command, Print Env command.
Enrico Tassi [Tue, 25 Jan 2005 09:26:01 +0000 (09:26 +0000)]
- added code for Coercion command, Print Env command.
- better error report in matitac

20 years ago- avoid redefinition of the same uri (checked in add_*_to_worls)
Stefano Zacchiroli [Mon, 24 Jan 2005 16:22:32 +0000 (16:22 +0000)]
- avoid redefinition of the same uri (checked in add_*_to_worls)
- defined add_inductive_def_to_world
- append owner to baseuri to minimize uri conflicts
- do not clear console!

20 years agouses CicPp.ppsort
Stefano Zacchiroli [Mon, 24 Jan 2005 16:20:29 +0000 (16:20 +0000)]
uses CicPp.ppsort

20 years ago- removed ancient debugging prints
Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]
- removed ancient debugging prints

20 years ago- renamed Term_not_found exception (useless) with Object_not_found
Stefano Zacchiroli [Mon, 24 Jan 2005 16:17:33 +0000 (16:17 +0000)]
- renamed Term_not_found exception (useless) with Object_not_found
  (now used)
- added getter exception handling. Now, hopefully, we will no longer see
  Pxp_types.At exception, but more meaningful ones (like Object_not_found)
- added in_libary which checks if an object exists (either in cache
  or via getter)
- in_cache: removed old debugging messages

20 years ago- added handling of exceptions embedded in xml documents (usually coming
Stefano Zacchiroli [Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)]
- added handling of exceptions embedded in xml documents (usually coming
  from http_getter)
- added exception Getter_failure which wraps the above exception
- added exception Parser_failure for generic errors
- removed useless EmptyUri exception

20 years agoexception carried in response xml documents are now split in two attributes:
Stefano Zacchiroli [Mon, 24 Jan 2005 16:13:00 +0000 (16:13 +0000)]
exception carried in response xml documents are now split in two attributes:
"helm:exception" (exception name) and "helm:exception_arg" (exception
argument)

20 years agoadded helm:exception handling of Http_getter_types.Key_not_found
Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]
added helm:exception handling of Http_getter_types.Key_not_found

20 years ago- sync with the new ApplyTransformation API
Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]
- sync with the new ApplyTransformation API

20 years ago- Changed ApplyTransformation API to return both the mathml and acic,
Enrico Tassi [Fri, 21 Jan 2005 11:49:03 +0000 (11:49 +0000)]
- Changed ApplyTransformation API to return both the mathml and acic,
  plus all the related tables
- Added the "Coercion" keyword to CicTextualParser2

20 years agosnapshot, notably:
Stefano Zacchiroli [Fri, 21 Jan 2005 09:40:48 +0000 (09:40 +0000)]
snapshot, notably:
- attributes support
- new ApplyTransformation interface
- simil-coma commit, browser is partially implemented :(

20 years agouniformed prototype of mml_of_cic_{object,sequent}
Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]
uniformed prototype of mml_of_cic_{object,sequent}

20 years agosyntax changes: "." at the end of the phrase instead of ";;"
Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]
syntax changes: "." at the end of the phrase instead of ";;"

20 years agoattributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]
attributes support

20 years ago- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]
- attributes support
- removed ancient debug prints

20 years agoattributes support (not yet in the pretty printer)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]
attributes support (not yet in the pretty printer)

20 years ago- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]
- attributes support
- default instance is 0 (not -1 !)

20 years agoattributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]
attributes support

20 years agoadded attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]
added attributes support

20 years ago- added string_of_sort
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]
- added string_of_sort
- attributes support