]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years ago* setpassword passwords swapped
Luca Padovani [Thu, 27 May 2004 11:08:21 +0000 (11:08 +0000)]
* setpassword passwords swapped

19 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

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

19 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)

19 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.

19 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.

19 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.

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

19 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.

19 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.

19 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

19 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 "/"

19 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

19 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

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

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

19 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

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

19 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)

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

19 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

19 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

19 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

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

19 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

19 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

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

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

19 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

19 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

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

19 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 ***

20 years agoAdding file newConstraint
Andrea Asperti [Mon, 10 May 2004 09:43:55 +0000 (09:43 +0000)]
Adding file newConstraint
The file contains functions for computing prefixes and related
stuff, required by the new management of matching.

20 years agoAdding file match_concl
Andrea Asperti [Mon, 10 May 2004 09:40:33 +0000 (09:40 +0000)]
Adding file match_concl
the file contains:
   - functions executing must, just and only constraints on the mysql
     data base;
   - the general function cmatch for retrieving all statements matching
     a given conclusion

20 years agosnapshot (notably: first working version of the console)
Stefano Zacchiroli [Tue, 4 May 2004 10:47:10 +0000 (10:47 +0000)]
snapshot (notably: first working version of the console)

20 years ago- moved up in the grammar precedences command entry so that sequence of
Stefano Zacchiroli [Tue, 4 May 2004 10:46:39 +0000 (10:46 +0000)]
- moved up in the grammar precedences command entry so that sequence of
  commands are not permitted
- added parsing of "abort" command

20 years agoremoved traliling dot in command pretty printer, now it's added by the
Stefano Zacchiroli [Tue, 4 May 2004 10:45:54 +0000 (10:45 +0000)]
removed traliling dot in command pretty printer, now it's added by the
tactical pp

20 years agoadded Abort and Check commands
Stefano Zacchiroli [Fri, 30 Apr 2004 14:00:15 +0000 (14:00 +0000)]
added Abort and Check commands

20 years agoembedded commands ast into tacticals ast
Stefano Zacchiroli [Fri, 30 Apr 2004 09:25:36 +0000 (09:25 +0000)]
embedded commands ast into tacticals ast

20 years ago- moved command as sub-entries of tactical grammars (as per tactics)
Stefano Zacchiroli [Fri, 30 Apr 2004 09:24:49 +0000 (09:24 +0000)]
- moved command as sub-entries of tactical grammars (as per tactics)

20 years agosnapshot
Stefano Zacchiroli [Fri, 30 Apr 2004 08:23:12 +0000 (08:23 +0000)]
snapshot

20 years ago- moved applyTransformation initialization code to the relevant library
Stefano Zacchiroli [Thu, 29 Apr 2004 16:15:25 +0000 (16:15 +0000)]
- moved applyTransformation initialization code to the relevant library
- decoupled termViewer from ChosenTransformer

20 years agomoved here initialization code (previously in gTopLevel/termViewer.ml)
Stefano Zacchiroli [Thu, 29 Apr 2004 16:14:33 +0000 (16:14 +0000)]
moved here initialization code (previously in gTopLevel/termViewer.ml)

20 years agosnapshot
Stefano Zacchiroli [Thu, 29 Apr 2004 13:59:11 +0000 (13:59 +0000)]
snapshot

20 years ago- added a configuration variable for selecting between fresh instances
Stefano Zacchiroli [Thu, 29 Apr 2004 13:55:31 +0000 (13:55 +0000)]
- added a configuration variable for selecting between fresh instances
  for numbers or not (set by default to a single instance)

20 years agosnapshot
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:38 +0000 (20:45 +0000)]
snapshot

20 years agoadded a TODO comment
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:16 +0000 (20:45 +0000)]
added a TODO comment

20 years agorebuilt
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:31 +0000 (15:04 +0000)]
rebuilt

20 years agoadded extra "id" parameter for input_or_locate_uri callback
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:11 +0000 (15:04 +0000)]
added extra "id" parameter for input_or_locate_uri callback

20 years ago- split logic operators away from aritmetic ones so that
Stefano Zacchiroli [Wed, 28 Apr 2004 14:11:51 +0000 (14:11 +0000)]
- split logic operators away from aritmetic ones so that
   \forall n:nat. n > 0 \or n = 0
  is parsed "correctly"

20 years agoremoved file:// prefix from local_library key, hopefully it isn't useful
Stefano Zacchiroli [Wed, 28 Apr 2004 14:00:42 +0000 (14:00 +0000)]
removed file:// prefix from local_library key, hopefully it isn't useful

20 years agosnapshot
Stefano Zacchiroli [Fri, 23 Apr 2004 14:54:46 +0000 (14:54 +0000)]
snapshot

20 years agogt URL pointed to lt
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 12:57:29 +0000 (12:57 +0000)]
gt URL pointed to lt

20 years agoUniverses introduction
Enrico Tassi [Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)]
Universes introduction

20 years agordfly hardcoded URL changed from mowgli.cs.unibo.it to localhost
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 10:03:12 +0000 (10:03 +0000)]
rdfly hardcoded URL changed from mowgli.cs.unibo.it to localhost

20 years agoexpandasking parameter passed to UWOBO.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 17:00:31 +0000 (17:00 +0000)]
expandasking parameter passed to UWOBO.