]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agotheory:path/index.theory are not rewritten to theory:/path.theory
Claudio Sacerdoti Coen [Mon, 31 May 2004 10:56:06 +0000 (10:56 +0000)]
theory:path/index.theory are not rewritten to theory:/path.theory
if theory:path/index.theory exists in the database.

20 years agoNew filtering function for "Auto" tactic using "just costraints"
Matteo Selmi [Mon, 31 May 2004 09:08:29 +0000 (09:08 +0000)]
New filtering function for "Auto" tactic using "just costraints"

20 years agoBack compatibility code introduced:
Claudio Sacerdoti Coen [Sun, 30 May 2004 22:14:49 +0000 (22:14 +0000)]
Back compatibility code introduced:
 1. the ls method maps a theory theory:/path/filename.theory
    to theory:/path/filename/index.theory iff there exists at least
    one object of the form cic:/path/filename/*
 2. the getter handles every URI theory:/path/filename/index.theory as
    the normalized URI theory:/path/filename.theory

20 years agoThe theory index.theory, if present, is shown at the beginning of the
Claudio Sacerdoti Coen [Sun, 30 May 2004 22:10:00 +0000 (22:10 +0000)]
The theory index.theory, if present, is shown at the beginning of the
listing.

20 years ago* makeProofTreeURL ported to the new interface
Luca Padovani [Fri, 28 May 2004 15:02:09 +0000 (15:02 +0000)]
* makeProofTreeURL ported to the new interface

20 years ago.body removed from bread crumb trail
Claudio Sacerdoti Coen [Fri, 28 May 2004 14:27:41 +0000 (14:27 +0000)]
.body removed from bread crumb trail

20 years agoLinks in the control frame when the URI ends with .body are now handled
Claudio Sacerdoti Coen [Fri, 28 May 2004 14:12:21 +0000 (14:12 +0000)]
Links in the control frame when the URI ends with .body are now handled
correctly (i.e. the .body is removed if meaningless, as for the proof-checker
or the metadata).

20 years ago<xsl:import href="toplevel_header.xsl"/>
Claudio Sacerdoti Coen [Fri, 28 May 2004 13:39:52 +0000 (13:39 +0000)]
<xsl:import href="toplevel_header.xsl"/>
moved here from show_dc.xsl

20 years ago<h1> ==> <h3>
Claudio Sacerdoti Coen [Fri, 28 May 2004 13:27:15 +0000 (13:27 +0000)]
<h1> ==> <h3>

20 years agostylesheet L added to the metadata chain
Claudio Sacerdoti Coen [Fri, 28 May 2004 13:20:18 +0000 (13:20 +0000)]
stylesheet L added to the metadata chain

20 years agobread crumb trail added
Claudio Sacerdoti Coen [Fri, 28 May 2004 13:18:36 +0000 (13:18 +0000)]
bread crumb trail added

20 years agometadataLib.xsl merged into metadataControl.xsl
Claudio Sacerdoti Coen [Fri, 28 May 2004 12:45:18 +0000 (12:45 +0000)]
metadataLib.xsl merged into metadataControl.xsl

20 years agoDead code removed.
Claudio Sacerdoti Coen [Fri, 28 May 2004 12:38:47 +0000 (12:38 +0000)]
Dead code removed.

20 years agodefaults.js no longer in use
Claudio Sacerdoti Coen [Fri, 28 May 2004 12:32:39 +0000 (12:32 +0000)]
defaults.js no longer in use

20 years agoFiles control.js graphLinks.js utils.js no longer in use.
Claudio Sacerdoti Coen [Fri, 28 May 2004 12:21:14 +0000 (12:21 +0000)]
Files control.js graphLinks.js utils.js no longer in use.

20 years agoDead code inclusion removed.
Claudio Sacerdoti Coen [Fri, 28 May 2004 12:19:18 +0000 (12:19 +0000)]
Dead code inclusion removed.

20 years agoNo longer in use.
Claudio Sacerdoti Coen [Fri, 28 May 2004 10:47:07 +0000 (10:47 +0000)]
No longer in use.

20 years agoNo longer in use.
Claudio Sacerdoti Coen [Fri, 28 May 2004 10:39:31 +0000 (10:39 +0000)]
No longer in use.

20 years agols2html.xsl no longer in use
Claudio Sacerdoti Coen [Fri, 28 May 2004 10:36:09 +0000 (10:36 +0000)]
ls2html.xsl no longer in use

20 years agoForm to choose the number of nodes to show removed ;-(
Claudio Sacerdoti Coen [Thu, 27 May 2004 17:55:33 +0000 (17:55 +0000)]
Form to choose the number of nodes to show removed ;-(

20 years ago&2C ==> %2C
Claudio Sacerdoti Coen [Thu, 27 May 2004 17:45:03 +0000 (17:45 +0000)]
&2C ==> %2C

20 years agoDead code removed.
Claudio Sacerdoti Coen [Thu, 27 May 2004 17:42:12 +0000 (17:42 +0000)]
Dead code removed.

20 years agoNew HELM interface almost stable.
Claudio Sacerdoti Coen [Thu, 27 May 2004 17:27:52 +0000 (17:27 +0000)]
New HELM interface almost stable.

20 years ago* it is now possible to set multiple parameters upon creation (or cloning)
Luca Padovani [Thu, 27 May 2004 15:04:33 +0000 (15:04 +0000)]
* it is now possible to set multiple parameters upon creation (or cloning)
  of a new profile

20 years ago* setpassword passwords swapped
Luca Padovani [Thu, 27 May 2004 11:08:21 +0000 (11:08 +0000)]
* setpassword passwords swapped

20 years ago* implemented setparams method for setting multiple parameters at once
Luca Padovani [Thu, 27 May 2004 09:24:03 +0000 (09:24 +0000)]
* implemented setparams method for setting multiple parameters at once

20 years ago...
Claudio Sacerdoti Coen [Wed, 26 May 2004 18:07:58 +0000 (18:07 +0000)]
...

20 years agoparam.processorURL added (need by the search engine)
Claudio Sacerdoti Coen [Wed, 26 May 2004 18:07:00 +0000 (18:07 +0000)]
param.processorURL added (need by the search engine)

20 years agotarget="_top" added to Search.
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:57:56 +0000 (17:57 +0000)]
target="_top" added to Search.

20 years agoLink to the search-engine hard-coded.
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:56:57 +0000 (17:56 +0000)]
Link to the search-engine hard-coded.

20 years agoMajor interface upgrade still going on. But we are approaching the end of the
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:54:36 +0000 (17:54 +0000)]
Major interface upgrade still going on. But we are approaching the end of the
tunnel.

20 years agoNew icons.
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:54:11 +0000 (17:54 +0000)]
New icons.

20 years agoMajor interface upgrade still going on. But we are approaching the end of
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:51:38 +0000 (17:51 +0000)]
Major interface upgrade still going on. But we are approaching the end of
the tunnel.

20 years agoBug fixed: ls?baseuri=(cic|theory):/a/ also returned theory:/a.theory.
Claudio Sacerdoti Coen [Wed, 26 May 2004 17:48:27 +0000 (17:48 +0000)]
Bug fixed: ls?baseuri=(cic|theory):/a/ also returned theory:/a.theory.

20 years ago* getparams returns annotated pairs key,values
Luca Padovani [Wed, 26 May 2004 16:26:56 +0000 (16:26 +0000)]
* getparams returns annotated pairs key,values

20 years agobugfix in /ls: removed double trailing "/"
Stefano Zacchiroli [Wed, 26 May 2004 15:37:45 +0000 (15:37 +0000)]
bugfix in /ls: removed double trailing "/"

20 years agoported to regexp based /ls method
Stefano Zacchiroli [Wed, 26 May 2004 15:30:08 +0000 (15:30 +0000)]
ported to regexp based /ls method

20 years agochanged /ls method so that regular expressions are used instead of plain
Stefano Zacchiroli [Wed, 26 May 2004 15:29:42 +0000 (15:29 +0000)]
changed /ls method so that regular expressions are used instead of plain
URIs

20 years agoMajor interface improvements.
Claudio Sacerdoti Coen [Wed, 26 May 2004 14:53:30 +0000 (14:53 +0000)]
Major interface improvements.

20 years ago* bumped to new version
Luca Padovani [Wed, 26 May 2004 09:08:48 +0000 (09:08 +0000)]
* bumped to new version

20 years ago* added external documentation in tex format
Luca Padovani [Wed, 26 May 2004 09:06:58 +0000 (09:06 +0000)]
* added external documentation in tex format
* true=>public and false=>private for permissions

20 years agoJSMmenu links fixed.
Claudio Sacerdoti Coen [Wed, 26 May 2004 09:00:27 +0000 (09:00 +0000)]
JSMmenu links fixed.

20 years ago###############################################################
Luca Padovani [Tue, 25 May 2004 17:56:07 +0000 (17:56 +0000)]
###############################################################
### Partial major upgrade of the HELM/MoWGLI Web interface. ###
###############################################################

WARNING: requires the new UWOBO profiles.

Known bugs:

 1. the JSMmenu for graphs is broken
 2. the configuration stuff is utterly broken: you should rely on
    the default configuration
 3. only HTML has been tested (MathML and ProofTrees are broken for
    sure)
 4. dead code everywhere (e.g. almost all the existent
    javascript code; several tokens in links_library.xsl)

20 years agoNew: UWOBO profiles added.
Luca Padovani [Tue, 25 May 2004 17:54:03 +0000 (17:54 +0000)]
New: UWOBO profiles added.

20 years agowritten a new sort function to postpone the resolution of some types of the goals
Matteo Selmi [Tue, 25 May 2004 07:07:19 +0000 (07:07 +0000)]
written a new sort function to postpone the resolution of some types of the goals

20 years agodon't remove documentation on "make dist" so that documentation will be
Stefano Zacchiroli [Mon, 24 May 2004 12:53:22 +0000 (12:53 +0000)]
don't remove documentation on "make dist" so that documentation will be
part of the generated tarball

20 years ago* setprofileparam ==> setparam
Luca Padovani [Mon, 24 May 2004 12:49:58 +0000 (12:49 +0000)]
* setprofileparam ==> setparam
* serialization/deserialization of the profile file implemented (write-through
  semantics)
* cloning of a profile fixed

20 years agoadded hostname resolution entry
Stefano Zacchiroli [Mon, 24 May 2004 12:47:36 +0000 (12:47 +0000)]
added hostname resolution entry

20 years agoimplemented hostname resolution for "addr" parameter
Stefano Zacchiroli [Mon, 24 May 2004 12:46:57 +0000 (12:46 +0000)]
implemented hostname resolution for "addr" parameter

20 years agorewritten "start" comment, now is almost decent
Stefano Zacchiroli [Mon, 24 May 2004 12:46:40 +0000 (12:46 +0000)]
rewritten "start" comment, now is almost decent

20 years agoemptied implementing all items
Stefano Zacchiroli [Mon, 24 May 2004 12:46:24 +0000 (12:46 +0000)]
emptied implementing all items

20 years agoremoved spurious messages
Stefano Zacchiroli [Mon, 24 May 2004 12:46:15 +0000 (12:46 +0000)]
removed spurious messages

20 years ago- ported to latest API
Stefano Zacchiroli [Mon, 24 May 2004 12:45:56 +0000 (12:45 +0000)]
- ported to latest API
- bumped copyright info

20 years ago- added basic_auth.ml example
Stefano Zacchiroli [Mon, 24 May 2004 12:45:33 +0000 (12:45 +0000)]
- added basic_auth.ml example
- restyled examples list

20 years agodebian snapshot (towards a release)
Stefano Zacchiroli [Mon, 24 May 2004 12:22:17 +0000 (12:22 +0000)]
debian snapshot (towards a release)

20 years agoadded OO interface
Stefano Zacchiroli [Mon, 24 May 2004 12:15:09 +0000 (12:15 +0000)]
added OO interface

20 years ago* preliminary version of profile management
Luca Padovani [Sat, 22 May 2004 07:01:09 +0000 (07:01 +0000)]
* preliminary version of profile management

20 years ago* updated respond_error messages after API change in ocaml-http 0.0.9
Luca Padovani [Sat, 22 May 2004 07:00:06 +0000 (07:00 +0000)]
* updated respond_error messages after API change in ocaml-http 0.0.9

20 years agoAdded a sort function to decide the order of theorems to try in the tactic "auto".
Matteo Selmi [Fri, 21 May 2004 16:44:53 +0000 (16:44 +0000)]
Added a sort function to decide the order of theorems to try in the tactic "auto".

20 years agoadded file locking while writing configuration to file (save_to)
Stefano Zacchiroli [Thu, 20 May 2004 17:17:24 +0000 (17:17 +0000)]
added file locking while writing configuration to file (save_to)

20 years agoopen Helm_registry per default
Stefano Zacchiroli [Thu, 20 May 2004 17:16:56 +0000 (17:16 +0000)]
open Helm_registry per default

20 years agobumped copyright years
Stefano Zacchiroli [Thu, 20 May 2004 16:55:11 +0000 (16:55 +0000)]
bumped copyright years

20 years agoChanged mapping keys <-> environment variables, mixed case envvars are
Stefano Zacchiroli [Thu, 20 May 2004 16:30:32 +0000 (16:30 +0000)]
Changed mapping keys <-> environment variables, mixed case envvars are
now used.

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 16:20:21 +0000 (16:20 +0000)]
ported to latest ocaml-http API

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 16:12:44 +0000 (16:12 +0000)]
ported to latest ocaml-http API

20 years agoreverted code parameter on respond function to its original optionality
Stefano Zacchiroli [Thu, 20 May 2004 16:02:25 +0000 (16:02 +0000)]
reverted code parameter on respond function to its original optionality

20 years agorebuilt
Stefano Zacchiroli [Thu, 20 May 2004 16:02:02 +0000 (16:02 +0000)]
rebuilt

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 15:50:19 +0000 (15:50 +0000)]
ported to latest ocaml-http API

20 years agowritten entry for 0.0.9
Stefano Zacchiroli [Thu, 20 May 2004 15:45:21 +0000 (15:45 +0000)]
written entry for 0.0.9

20 years agorestyled API so that respond_* are statically typechecked
Stefano Zacchiroli [Thu, 20 May 2004 15:45:08 +0000 (15:45 +0000)]
restyled API so that respond_* are statically typechecked

20 years ago- changed API so that respond_* are statically type checked for correct
Stefano Zacchiroli [Thu, 20 May 2004 15:44:43 +0000 (15:44 +0000)]
- changed API so that respond_* are statically type checked for correct
  parameter instantiation
- restyled a lot of code

20 years agoadded support for HEAD requests
Stefano Zacchiroli [Thu, 20 May 2004 15:44:01 +0000 (15:44 +0000)]
added support for HEAD requests

20 years agohttp basic authentication example
Stefano Zacchiroli [Thu, 20 May 2004 14:33:20 +0000 (14:33 +0000)]
http basic authentication example

20 years agoadded support for HTTP (Basic) authentication
Stefano Zacchiroli [Thu, 20 May 2004 14:30:48 +0000 (14:30 +0000)]
added support for HTTP (Basic) authentication

20 years ago- added support for HTTP (Basic) authentication
Stefano Zacchiroli [Thu, 20 May 2004 14:30:27 +0000 (14:30 +0000)]
- added support for HTTP (Basic) authentication
- simplified usage of some internal optional parameters

20 years ago* hbugs moved in ocaml
Luca Padovani [Thu, 20 May 2004 12:10:18 +0000 (12:10 +0000)]
* hbugs moved in ocaml

20 years agoadded some nested sections in order to test "ls" method
Stefano Zacchiroli [Thu, 20 May 2004 12:08:08 +0000 (12:08 +0000)]
added some nested sections in order to test "ls" method

20 years ago- added "has" method
Stefano Zacchiroli [Thu, 20 May 2004 12:07:37 +0000 (12:07 +0000)]
- added "has" method
- added "ls" method
- added "?prefix" parameter to "fold", "iter" and "to_list" methods

20 years agoadded helm-pxp, now needed
Stefano Zacchiroli [Thu, 20 May 2004 12:06:35 +0000 (12:06 +0000)]
added helm-pxp, now needed

20 years agoexpanded content of old topfind
Stefano Zacchiroli [Thu, 20 May 2004 09:39:04 +0000 (09:39 +0000)]
expanded content of old topfind

20 years agono longer needed
Stefano Zacchiroli [Thu, 20 May 2004 09:32:28 +0000 (09:32 +0000)]
no longer needed

20 years agoadded iterators over registry contents (fold, iter, to_list)
Stefano Zacchiroli [Thu, 20 May 2004 09:27:06 +0000 (09:27 +0000)]
added iterators over registry contents (fold, iter, to_list)

20 years agoTempative version: every link is now opened in a new window.
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:51:16 +0000 (15:51 +0000)]
Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

20 years agoBug fixed: middle-clicking over links in the listing frames should now
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:45:15 +0000 (15:45 +0000)]
Bug fixed: middle-clicking over links in the listing frames should now
work on any browser.

20 years agoTempative version: every link is now opened in a new window.
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:44:37 +0000 (15:44 +0000)]
Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

20 years agofirst moogle template checkin
Andrea Asperti [Wed, 19 May 2004 14:39:42 +0000 (14:39 +0000)]
first moogle template checkin

20 years ago* the input of the function mkMetaTheoryURL must an (unquoted) URI. Fixed.
Claudio Sacerdoti Coen [Tue, 18 May 2004 17:12:05 +0000 (17:12 +0000)]
* the input of the function mkMetaTheoryURL must an (unquoted) URI. Fixed.

20 years ago* the URI passed to the rdfly deamon is now CICURI, except that quoting
Claudio Sacerdoti Coen [Tue, 18 May 2004 16:06:07 +0000 (16:06 +0000)]
* the URI passed to the rdfly deamon is now CICURI, except that quoting
  rules are different.

20 years ago* [Luca] string concatenation now made using String.concat instead of
Claudio Sacerdoti Coen [Tue, 18 May 2004 15:57:23 +0000 (15:57 +0000)]
* [Luca] string concatenation now made using String.concat instead of
  List.fold_left

20 years agoNuova implementazione di Auto "breadth-first".
Andrea Asperti [Tue, 18 May 2004 13:25:35 +0000 (13:25 +0000)]
Nuova implementazione di Auto "breadth-first".

20 years agoxml:base and helm:base are now generated only for theories.
Claudio Sacerdoti Coen [Tue, 18 May 2004 09:16:31 +0000 (09:16 +0000)]
xml:base and helm:base are now generated only for theories.

20 years ago* tactics/Makefile fixed (to remove duplicate .mli files)
Claudio Sacerdoti Coen [Tue, 18 May 2004 08:56:50 +0000 (08:56 +0000)]
* tactics/Makefile fixed (to remove duplicate .mli files)
* .depend regenerated

20 years agoBug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
Claudio Sacerdoti Coen [Tue, 18 May 2004 08:39:54 +0000 (08:39 +0000)]
Bug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
were full URIs (with also the filename at the end). Fixed by using
Filename.dirname (that seems to work also with generic URIs).

20 years agoAdded a filter for uris in tactic "auto".
Matteo Selmi [Mon, 17 May 2004 20:58:56 +0000 (20:58 +0000)]
Added a filter for uris in tactic "auto".
Uris of theorems containing, in the conclusion or in the hypothesis, constants not present in the proof (hypothesis or conclusion) are filtered out.

20 years agoAdded support for xml base(s) URL and URI. The getter now adds these two
Stefano Zacchiroli [Mon, 17 May 2004 17:48:33 +0000 (17:48 +0000)]
Added support for xml base(s) URL and URI. The getter now adds these two
attributes (hopefully) on the first open tag

20 years agofirst check in of statefulProofEngine
Stefano Zacchiroli [Mon, 17 May 2004 12:30:19 +0000 (12:30 +0000)]
first check in of statefulProofEngine

20 years agobugfix: remove trailing slashes from dtd_base_urls
Stefano Zacchiroli [Mon, 17 May 2004 11:35:37 +0000 (11:35 +0000)]
bugfix: remove trailing slashes from dtd_base_urls

20 years ago- some code patched
Ferruccio Guidi [Thu, 13 May 2004 13:32:12 +0000 (13:32 +0000)]
- some code patched
- mathql documentation updated

20 years agochanged proofStatus so that uri component is optional (useful to start an
Stefano Zacchiroli [Thu, 13 May 2004 12:59:43 +0000 (12:59 +0000)]
changed proofStatus so that uri component is optional (useful to start an
unnamed proof or leave the possibility of postpone uri choice)

20 years ago*** empty log message ***
Andrea Asperti [Mon, 10 May 2004 13:31:57 +0000 (13:31 +0000)]
*** empty log message ***