]>
matita.cs.unibo.it Git - helm.git/log
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
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