]>
matita.cs.unibo.it Git - helm.git/log
Stefano Zacchiroli [Thu, 3 Feb 2005 10:40:49 +0000 (10:40 +0000)]
removed spurious load of a local gTopLevel.conf.xml
Stefano Zacchiroli [Wed, 2 Feb 2005 14:12:24 +0000 (14:12 +0000)]
- implemented inductive type rendering
- added hyperlinks on parameters
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
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
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
Stefano Zacchiroli [Tue, 1 Feb 2005 17:56:54 +0000 (17:56 +0000)]
removed useless parameter uri from mml_of_cic_object
Stefano Zacchiroli [Tue, 1 Feb 2005 17:55:53 +0000 (17:55 +0000)]
added mathml_ns
Stefano Zacchiroli [Tue, 1 Feb 2005 17:55:29 +0000 (17:55 +0000)]
enriched error message
Stefano Zacchiroli [Tue, 1 Feb 2005 17:54:49 +0000 (17:54 +0000)]
added strip_xpointer: remove trailing #xpointer from a UriManager.uri value
Enrico Tassi [Tue, 1 Feb 2005 15:40:15 +0000 (15:40 +0000)]
reverder change. no more owner passed to the locate.
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).
Enrico Tassi [Tue, 1 Feb 2005 13:47:00 +0000 (13:47 +0000)]
*** empty log message ***
Enrico Tassi [Tue, 1 Feb 2005 13:45:36 +0000 (13:45 +0000)]
added `Coer print_kind
Enrico Tassi [Tue, 1 Feb 2005 13:45:05 +0000 (13:45 +0000)]
Added Coer/Coercions print_kind
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
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
Enrico Tassi [Tue, 1 Feb 2005 11:46:31 +0000 (11:46 +0000)]
added the unregister method to the help page
Enrico Tassi [Tue, 1 Feb 2005 10:42:18 +0000 (10:42 +0000)]
fixed coercions
Enrico Tassi [Tue, 1 Feb 2005 10:05:52 +0000 (10:05 +0000)]
removed debug print
Enrico Tassi [Tue, 1 Feb 2005 10:05:14 +0000 (10:05 +0000)]
cosmetic fix to pp_location
Enrico Tassi [Mon, 31 Jan 2005 17:29:03 +0000 (17:29 +0000)]
added save_object_to_disk and basedir
Enrico Tassi [Mon, 31 Jan 2005 17:18:55 +0000 (17:18 +0000)]
added delift
Enrico Tassi [Mon, 31 Jan 2005 17:17:32 +0000 (17:17 +0000)]
added basedir and improved let{rec} syntax
Enrico Tassi [Mon, 31 Jan 2005 17:16:41 +0000 (17:16 +0000)]
better debug prints
Enrico Tassi [Mon, 31 Jan 2005 17:12:12 +0000 (17:12 +0000)]
added Basedir Ast
Enrico Tassi [Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)]
Added outtype inference to MutCase
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.
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
Enrico Tassi [Tue, 25 Jan 2005 09:28:50 +0000 (09:28 +0000)]
added list_obj and list_uri
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
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!
Stefano Zacchiroli [Mon, 24 Jan 2005 16:20:29 +0000 (16:20 +0000)]
uses CicPp.ppsort
Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]
- removed ancient debugging prints
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
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
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)
Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]
added helm:exception handling of Http_getter_types.Key_not_found
Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]
- sync with the new ApplyTransformation API
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
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 :(
Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]
uniformed prototype of mml_of_cic_{object,sequent}
Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]
syntax changes: "." at the end of the phrase instead of ";;"
Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]
attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]
- attributes support
- removed ancient debug prints
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]
attributes support (not yet in the pretty printer)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]
- attributes support
- default instance is 0 (not -1 !)
Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]
attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]
added attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]
- added string_of_sort
- attributes support
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:58 +0000 (09:20 +0000)]
- added attributes support
- uses string_of_sort from CicPp
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:09 +0000 (09:20 +0000)]
added attributes
Stefano Zacchiroli [Fri, 21 Jan 2005 09:19:02 +0000 (09:19 +0000)]
added attribute support (not yet in the parser)
Stefano Zacchiroli [Thu, 20 Jan 2005 10:33:50 +0000 (10:33 +0000)]
snapshot, notably:
- added hyperlink handling in check and proof window
- start implementation of cic browser
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)]
helmns -> helm_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:01 +0000 (10:32 +0000)]
- added rendering of constants/variable with/without body
Stefano Zacchiroli [Thu, 20 Jan 2005 10:31:25 +0000 (10:31 +0000)]
rendering fixes:
- does not assert false for a missing idref on a symbol (which is not
available when rendering ast coming from parsing)
- fixed pattern matching rendering
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:58 +0000 (10:26 +0000)]
- helmns -> helm_ns
- added xlink_ns
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:06 +0000 (10:26 +0000)]
added cast rendering (used in check window by gTopLevel/matita)
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:59 +0000 (10:24 +0000)]
added URI concrete syntax
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:44 +0000 (10:24 +0000)]
added cmdline alias "command" for "tactica"
Enrico Tassi [Wed, 19 Jan 2005 16:03:27 +0000 (16:03 +0000)]
coercion application
Enrico Tassi [Wed, 19 Jan 2005 15:48:44 +0000 (15:48 +0000)]
fix coercGraph.mli
Enrico Tassi [Wed, 19 Jan 2005 15:26:12 +0000 (15:26 +0000)]
fixed #xpointer handling in uri_of_string. new examples :
"cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |]
"cic:/a/b/c.ind#xpointer(1/1)" =>
[| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |]
"cic:/a/b/c.ind#xpointer(1/1/1)" =>
[| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]
Enrico Tassi [Wed, 19 Jan 2005 15:23:12 +0000 (15:23 +0000)]
Added coercion handling module
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:56 +0000 (18:18 +0000)]
license template
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:35 +0000 (18:18 +0000)]
read uri from cmdline
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:00 +0000 (18:18 +0000)]
added pp_location (pretty printer of ast location)
Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]
added script support
Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]
added latex style comment, with start token "%%"
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]
removed spurious debugging prints
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]
snapshot, notably:
- first commit of matitac
Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]
fixed comments
Stefano Zacchiroli [Mon, 17 Jan 2005 16:24:22 +0000 (16:24 +0000)]
- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
- changed usage string so that it is a well fermod XHTML document (added
namespace, quoted ampersands)
Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]
new cicEnvironment implementation
Stefano Zacchiroli [Mon, 17 Jan 2005 16:23:26 +0000 (16:23 +0000)]
No longer return HTTP 400 answers or non-xml answers: all document returned
by the getter are now XHTML documents, possibly with the addition of an
attribute helm:exception on the root <html> element in the
http://www.cs.unibo.it/helm namespace. The presence of such an attribute
means that an exception has occured, its value is meant to be a string
encoding of the relevant ocaml exception
Stefano Zacchiroli [Mon, 17 Jan 2005 14:53:03 +0000 (14:53 +0000)]
first (almost) working version: apparently, only generation of coinductive
eliminators does not typecheck
Stefano Zacchiroli [Fri, 14 Jan 2005 17:35:26 +0000 (17:35 +0000)]
snapshot, notably:
- changed interface, now returns a Cic.obj
- added consistency check between generated body and type
Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]
snapshot (1st commit of fix body generation)
Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]
fixed clean_and_fill
Enrico Tassi [Wed, 12 Jan 2005 14:56:46 +0000 (14:56 +0000)]
fixed bug in fill_and_clean (now the helper universes_of_obj knows that
the uri passed as the first parameter can't be in the environment and it
doesn't requests it)
Stefano Zacchiroli [Tue, 11 Jan 2005 16:11:12 +0000 (16:11 +0000)]
snapshot, notably:
- added support for inductive definitions
- prelimnary support for user searches
Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]
added fallback case (assertion failure) for unsupported Implicit annotations
Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]
added syntax for URIs
Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]
added search commands
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
- added syntax for URIs
Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]
added clean_and_fill, to be invoked on qed
Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]
snapshot, not yet completed, but ...
Stefano Zacchiroli [Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)]
- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
matching a context
Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]
cosmetic changes
Enrico Tassi [Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)]
added begin list and end list comments to help moogle search engine plugin
Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]
exported lift_from
Stefano Zacchiroli [Wed, 5 Jan 2005 14:06:41 +0000 (14:06 +0000)]
snapshot
Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]
added an hyperlink to the input syntax page
Stefano Zacchiroli [Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)]
improved input syntax page with example queries of elim, match and hint
Stefano Zacchiroli [Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)]
added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)
Stefano Zacchiroli [Tue, 21 Dec 2004 15:49:03 +0000 (15:49 +0000)]
first commit (in the wrong place --by CSC) of induction principles generation
Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]
ignores example binaries
Stefano Zacchiroli [Thu, 9 Dec 2004 20:31:24 +0000 (20:31 +0000)]
ported to new format of Parse_error exception (which includes error position)
Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]
(dummy) porting to universes