]>
matita.cs.unibo.it Git - helm.git/log
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:48 +0000 (23:45 +0000)]
debian: rebuilt against ocaml 3.08.3
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:33 +0000 (23:45 +0000)]
remove x_gdome_caml.c generated source on "clean"
Stefano Zacchiroli [Fri, 25 Mar 2005 23:44:44 +0000 (23:44 +0000)]
debian: rebuilt against ocaml 3.08.2
Claudio Sacerdoti Coen [Tue, 22 Mar 2005 16:05:54 +0000 (16:05 +0000)]
Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.
Stefano Zacchiroli [Wed, 16 Mar 2005 16:33:10 +0000 (16:33 +0000)]
- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
- bugfix: security, no longer subject to directory traversal (!)
Stefano Zacchiroli [Wed, 16 Mar 2005 16:21:44 +0000 (16:21 +0000)]
user smaller font in result page
Stefano Zacchiroli [Wed, 16 Mar 2005 16:17:03 +0000 (16:17 +0000)]
- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel
Stefano Zacchiroli [Wed, 16 Mar 2005 16:16:06 +0000 (16:16 +0000)]
make and clean also in html/
Stefano Zacchiroli [Wed, 16 Mar 2005 16:15:28 +0000 (16:15 +0000)]
removed old HTML files (tagged with "old_htmls")
Stefano Zacchiroli [Wed, 16 Mar 2005 15:57:25 +0000 (15:57 +0000)]
moogle.html is now generated, it do not needs to be in CVS
Stefano Zacchiroli [Wed, 16 Mar 2005 15:56:44 +0000 (15:56 +0000)]
generate HTML templates using XSLT starting from a bunch of .src files
Stefano Zacchiroli [Wed, 16 Mar 2005 15:50:35 +0000 (15:50 +0000)]
look and feel improvements
Stefano Zacchiroli [Wed, 16 Mar 2005 10:23:37 +0000 (10:23 +0000)]
- 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)
Stefano Zacchiroli [Tue, 15 Mar 2005 08:27:10 +0000 (08:27 +0000)]
- handle metavariables: if at least one of them is present, then the
cardinality constraint is not enforce
- commented out debugging prints
Stefano Zacchiroli [Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)]
bugfix when user query contains metas: their context should not be analyzed
as it were in main position
Stefano Zacchiroli [Fri, 11 Mar 2005 18:37:41 +0000 (18:37 +0000)]
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.
Stefano Zacchiroli [Wed, 9 Mar 2005 10:24:03 +0000 (10:24 +0000)]
added support for open terms in check
Stefano Zacchiroli [Wed, 9 Mar 2005 10:22:39 +0000 (10:22 +0000)]
support for terms with metas in check
Enrico Tassi [Mon, 14 Feb 2005 15:12:24 +0000 (15:12 +0000)]
added choose_uri method to console, used by the interpreter to implement the
hint command
Enrico Tassi [Mon, 14 Feb 2005 12:06:45 +0000 (12:06 +0000)]
Added heuristic in the Appl case, we beta-expand only if the argument list
does't contain metas.
Enrico Tassi [Mon, 14 Feb 2005 09:51:39 +0000 (09:51 +0000)]
Fixed remove operation and get_obj (that now correctly searches in the
unchecked_list).
Stefano Zacchiroli [Thu, 10 Feb 2005 16:12:17 +0000 (16:12 +0000)]
moved a debug print so that it is executed for each phrase
Stefano Zacchiroli [Thu, 10 Feb 2005 16:06:36 +0000 (16:06 +0000)]
adapted to optional comment lexer interface
Stefano Zacchiroli [Thu, 10 Feb 2005 15:54:44 +0000 (15:54 +0000)]
renaming "remove_term" -> "remove_obj"
Stefano Zacchiroli [Thu, 10 Feb 2005 15:54:00 +0000 (15:54 +0000)]
- fix in intro parsing
- avoid generating seq tactical for a 1-length sequences
Stefano Zacchiroli [Thu, 10 Feb 2005 15:52:22 +0000 (15:52 +0000)]
factorized tacticals separator and terminator
Stefano Zacchiroli [Thu, 10 Feb 2005 15:51:42 +0000 (15:51 +0000)]
added "unindex" to undo indexing of a single object
Stefano Zacchiroli [Thu, 10 Feb 2005 15:45:40 +0000 (15:45 +0000)]
bugfix: method 'advance' now took in input concrete syntax since atm
pretty printing is not the inverse operation of parsing
Stefano Zacchiroli [Thu, 10 Feb 2005 15:44:34 +0000 (15:44 +0000)]
changed toolbar window type
Stefano Zacchiroli [Thu, 10 Feb 2005 15:44:20 +0000 (15:44 +0000)]
bugfix: avoid executing tactic for the script twice
Stefano Zacchiroli [Thu, 10 Feb 2005 09:55:02 +0000 (09:55 +0000)]
removed spurious dependency on Dbi_mysql
Stefano Zacchiroli [Wed, 9 Feb 2005 15:07:37 +0000 (15:07 +0000)]
added script support a la coqide
Stefano Zacchiroli [Wed, 9 Feb 2005 15:07:22 +0000 (15:07 +0000)]
- 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
Stefano Zacchiroli [Wed, 9 Feb 2005 15:06:25 +0000 (15:06 +0000)]
moved lockScript to MatitaScript module
Stefano Zacchiroli [Tue, 8 Feb 2005 21:53:41 +0000 (21:53 +0000)]
0.1.0-1 entry
Stefano Zacchiroli [Tue, 8 Feb 2005 21:50:44 +0000 (21:50 +0000)]
strip debian version from META version
Stefano Zacchiroli [Tue, 8 Feb 2005 21:43:30 +0000 (21:43 +0000)]
use wildcard in install target so that binary objects are installed only
when built
Stefano Zacchiroli [Tue, 8 Feb 2005 17:28:21 +0000 (17:28 +0000)]
added a missing unchecked_to_frozen (fixes a Not_found exception while
type checking without trust)
Enrico Tassi [Tue, 8 Feb 2005 15:47:49 +0000 (15:47 +0000)]
at_least now supports the ownerized tables
Stefano Zacchiroli [Tue, 8 Feb 2005 15:35:52 +0000 (15:35 +0000)]
added boxml namespace
Stefano Zacchiroli [Tue, 8 Feb 2005 12:16:04 +0000 (12:16 +0000)]
- changed license to lgpl
- bumped copyright
- improved ocamldoc comments
Stefano Zacchiroli [Tue, 8 Feb 2005 12:15:09 +0000 (12:15 +0000)]
debian changes target release 0.1.0
Stefano Zacchiroli [Tue, 8 Feb 2005 12:14:34 +0000 (12:14 +0000)]
included lgpl
Stefano Zacchiroli [Mon, 7 Feb 2005 15:24:07 +0000 (15:24 +0000)]
added TODO file
Stefano Zacchiroli [Mon, 7 Feb 2005 15:23:02 +0000 (15:23 +0000)]
added support for directory browsing in cicBrowser
Stefano Zacchiroli [Mon, 7 Feb 2005 15:22:44 +0000 (15:22 +0000)]
rebuilt
Stefano Zacchiroli [Mon, 7 Feb 2005 15:22:37 +0000 (15:22 +0000)]
connected change tactic (proof of concept)
Enrico Tassi [Mon, 7 Feb 2005 12:07:41 +0000 (12:07 +0000)]
removed chosenTransformer.ml*
Enrico Tassi [Mon, 7 Feb 2005 11:49:16 +0000 (11:49 +0000)]
removed chosenTransformer.mli
Enrico Tassi [Mon, 7 Feb 2005 10:25:53 +0000 (10:25 +0000)]
sync with Xml.pp
Stefano Zacchiroli [Fri, 4 Feb 2005 16:52:29 +0000 (16:52 +0000)]
fix join on multiple tables
Enrico Tassi [Fri, 4 Feb 2005 16:15:44 +0000 (16:15 +0000)]
fixed Gzip bug in Xml.pp
Enrico Tassi [Fri, 4 Feb 2005 16:13:28 +0000 (16:13 +0000)]
saves to gzip
Enrico Tassi [Fri, 4 Feb 2005 15:47:40 +0000 (15:47 +0000)]
added library table and owner tables handling in the SQL code
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
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
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
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
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)
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
Stefano Zacchiroli [Fri, 4 Feb 2005 13:58:53 +0000 (13:58 +0000)]
added gzip support to Xml
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
Enrico Tassi [Fri, 4 Feb 2005 13:01:29 +0000 (13:01 +0000)]
fix
Stefano Zacchiroli [Fri, 4 Feb 2005 12:11:07 +0000 (12:11 +0000)]
return also .types uri in getalluris/
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
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
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:50 +0000 (09:29 +0000)]
removed dep on mathql
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:03 +0000 (09:29 +0000)]
rebuilt
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:42 +0000 (09:28 +0000)]
- removed dependency on mathql
- cosmetic changes
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:07 +0000 (09:28 +0000)]
- added init method
- added default values for loglevel and logfile
Stefano Zacchiroli [Fri, 4 Feb 2005 09:27:30 +0000 (09:27 +0000)]
rebuild
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
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:46 +0000 (09:24 +0000)]
local_url predicate (recognize file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:01 +0000 (09:24 +0000)]
do not cache local resources (i.e. file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:23:27 +0000 (09:23 +0000)]
create path towards dbm file
Stefano Zacchiroli [Fri, 4 Feb 2005 09:15:40 +0000 (09:15 +0000)]
removed ancient mathql deps
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
Stefano Zacchiroli [Fri, 4 Feb 2005 09:14:32 +0000 (09:14 +0000)]
cosmetic changes
Stefano Zacchiroli [Thu, 3 Feb 2005 22:31:35 +0000 (22:31 +0000)]
target 0.1.0 changelog (not yet released ...)
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
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
Stefano Zacchiroli [Thu, 3 Feb 2005 22:20:29 +0000 (22:20 +0000)]
cosmetic changes (no longer open Neturl)
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:48 +0000 (22:19 +0000)]
removed Makefile.overrides
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:13 +0000 (22:19 +0000)]
rebuilt
Stefano Zacchiroli [Thu, 3 Feb 2005 22:19:00 +0000 (22:19 +0000)]
- moved ocamldoc comments in .mli
- added daemon_spec
Stefano Zacchiroli [Thu, 3 Feb 2005 22:18:26 +0000 (22:18 +0000)]
added warn and error for messaging
Stefano Zacchiroli [Thu, 3 Feb 2005 22:17:54 +0000 (22:17 +0000)]
added http_types.mli: Makefile.overrides is now useless
Stefano Zacchiroli [Thu, 3 Feb 2005 22:12:53 +0000 (22:12 +0000)]
removed useless dont_fork and obj_foo examples
Stefano Zacchiroli [Thu, 3 Feb 2005 22:12:18 +0000 (22:12 +0000)]
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
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
Stefano Zacchiroli [Thu, 3 Feb 2005 22:06:01 +0000 (22:06 +0000)]
added head_callback to access response status and headers in requests
Enrico Tassi [Thu, 3 Feb 2005 16:46:12 +0000 (16:46 +0000)]
fixed currentproof
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
Enrico Tassi [Thu, 3 Feb 2005 16:40:06 +0000 (16:40 +0000)]
MetadataDb.clean doesn't need ~owner since table names are ownerized ;)
Enrico Tassi [Thu, 3 Feb 2005 15:12:08 +0000 (15:12 +0000)]
owners table not needed
Enrico Tassi [Thu, 3 Feb 2005 14:32:22 +0000 (14:32 +0000)]
added new ownerize function
Enrico Tassi [Thu, 3 Feb 2005 14:31:59 +0000 (14:31 +0000)]
new metadataTypes interface (with ownerize function)
Enrico Tassi [Thu, 3 Feb 2005 13:14:04 +0000 (13:14 +0000)]
removed uri parameter from load_proof
Stefano Zacchiroli [Thu, 3 Feb 2005 10:43:22 +0000 (10:43 +0000)]
rebuilt