]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years agoadded support for setting debug and error callbacks
Stefano Zacchiroli [Thu, 13 Mar 2003 21:45:37 +0000 (21:45 +0000)]
added support for setting debug and error callbacks

21 years agobugfix: installs also i_gdome_xslt.ml, gdome_xslt_init.o and
Stefano Zacchiroli [Thu, 13 Mar 2003 21:44:28 +0000 (21:44 +0000)]
bugfix: installs also i_gdome_xslt.ml, gdome_xslt_init.o and
libmlgdome2-xslt.a

21 years agodebian release 0.0.4-3
Stefano Zacchiroli [Thu, 13 Mar 2003 21:43:45 +0000 (21:43 +0000)]
debian release 0.0.4-3

21 years agoAdded the completion of the macro's name.
Paolo Marinelli [Thu, 13 Mar 2003 18:20:08 +0000 (18:20 +0000)]
Added the completion of the macro's name.
To meet this goal, the abstract lexer has a new method: complete.
T(L)PushLexer doesn't implement this method. But there are two additional
classes: ITPushLexer and ILPushLexer. These are derived from TPushLexer and
LPushLexer. The only difference between the derived classes and their parents
is the implementation of the method complete.
TDictionary has a new method: complete. It's used by the lexers.
Now, in LPushLexer, long identifiers can be composed by these additional
character: '-' and '_'. To insert them as part of long identifiers, the
user has escape them with '\'.
Added a new node in the TML tree. It' name is 's' and represents a space.
It can be pushed only with a LPushLexer.

21 years agoThis xslt transforms the TML tree in TeX using a particular syntax:
Paolo Marinelli [Thu, 13 Mar 2003 17:44:48 +0000 (17:44 +0000)]
This xslt transforms the TML tree in TeX using a particular syntax:
  every node having the attribute Id, will be transformed in
  {\id{id value}{expansion of its children}}.

21 years agoreindented and recommented kindly
Stefano Zacchiroli [Thu, 13 Mar 2003 15:46:34 +0000 (15:46 +0000)]
reindented and recommented kindly

21 years agoinstalls also i_gomde_xslt.mli
Stefano Zacchiroli [Thu, 13 Mar 2003 15:12:08 +0000 (15:12 +0000)]
installs also i_gomde_xslt.mli

21 years agodebian release 0.0.4-2:
Stefano Zacchiroli [Thu, 13 Mar 2003 15:10:52 +0000 (15:10 +0000)]
debian release 0.0.4-2:
- installs also i_gdome_xslt.cmi

21 years ago- Some .cvsignore were missing
Claudio Sacerdoti Coen [Thu, 13 Mar 2003 14:50:21 +0000 (14:50 +0000)]
- Some .cvsignore were missing
- Backtracking on the few glib2 dependencies

21 years ago* removed .in files
Luca Padovani [Thu, 13 Mar 2003 14:33:57 +0000 (14:33 +0000)]
* removed .in files

21 years ago* removed GLIB 2 dependencies (GLIB 2 not used!)
Luca Padovani [Thu, 13 Mar 2003 14:31:05 +0000 (14:31 +0000)]
* removed GLIB 2 dependencies (GLIB 2 not used!)

21 years agoRemoved the line that sourced the personal configuration file of Zack.
Claudio Sacerdoti Coen [Thu, 13 Mar 2003 14:13:15 +0000 (14:13 +0000)]
Removed the line that sourced the personal configuration file of Zack.

21 years agoMathQL homepage added
Ferruccio Guidi [Thu, 13 Mar 2003 14:00:31 +0000 (14:00 +0000)]
MathQL homepage added

21 years ago* license update
Luca Padovani [Thu, 13 Mar 2003 13:52:32 +0000 (13:52 +0000)]
* license update

21 years ago* licenses updated
Luca Padovani [Thu, 13 Mar 2003 13:52:12 +0000 (13:52 +0000)]
* licenses updated

21 years ago* added license and copyright to every source file
Luca Padovani [Thu, 13 Mar 2003 11:50:00 +0000 (11:50 +0000)]
* added license and copyright to every source file
* fixes in the makefiles for distribution
* preparing for packaging

21 years ago* disable-shared doens't bother ocaml
Luca Padovani [Thu, 13 Mar 2003 10:44:35 +0000 (10:44 +0000)]
* disable-shared doens't bother ocaml

21 years agomoved uwobo sources to the root uwobo directory
Stefano Zacchiroli [Wed, 12 Mar 2003 18:37:49 +0000 (18:37 +0000)]
moved uwobo sources to the root uwobo directory

21 years agoremoved .cvswrappers
Stefano Zacchiroli [Wed, 12 Mar 2003 18:36:16 +0000 (18:36 +0000)]
removed .cvswrappers

21 years ago- reimplemented cache handling
Stefano Zacchiroli [Wed, 12 Mar 2003 18:06:07 +0000 (18:06 +0000)]
- reimplemented cache handling
- solved race condition issues (closes: bug#26)

21 years agoadded "output" parameter to gzip and gunzip used to specify target file
Stefano Zacchiroli [Wed, 12 Mar 2003 18:03:46 +0000 (18:03 +0000)]
added "output" parameter to gzip and gunzip used to specify target file
for compression and decompression

21 years agoadded support for patch_fun also for gzipped documents
Stefano Zacchiroli [Wed, 12 Mar 2003 18:03:07 +0000 (18:03 +0000)]
added support for patch_fun also for gzipped documents

21 years agoembedded configuration infos in usage string
Stefano Zacchiroli [Wed, 12 Mar 2003 18:02:04 +0000 (18:02 +0000)]
embedded configuration infos in usage string

21 years agoremoved dump_env in favour of env_to_string which return a string
Stefano Zacchiroli [Wed, 12 Mar 2003 18:01:47 +0000 (18:01 +0000)]
removed dump_env in favour of env_to_string which return a string
describing current environment

21 years ago- embedded configuration information in help string
Stefano Zacchiroli [Wed, 12 Mar 2003 18:01:04 +0000 (18:01 +0000)]
- embedded configuration information in help string
- bumped version to 0.2.1

21 years agorebuilt
Stefano Zacchiroli [Wed, 12 Mar 2003 18:00:12 +0000 (18:00 +0000)]
rebuilt

21 years agoremoved old java implementation
Stefano Zacchiroli [Wed, 12 Mar 2003 17:26:25 +0000 (17:26 +0000)]
removed old java implementation

21 years agotypo fixes in usage string
Stefano Zacchiroli [Wed, 12 Mar 2003 17:24:31 +0000 (17:24 +0000)]
typo fixes in usage string

21 years agoremoved an ancient debugging message
Stefano Zacchiroli [Wed, 12 Mar 2003 17:24:01 +0000 (17:24 +0000)]
removed an ancient debugging message

21 years agoadded generation of dot dependency graph
Stefano Zacchiroli [Wed, 12 Mar 2003 17:23:10 +0000 (17:23 +0000)]
added generation of dot dependency graph

21 years ago- bugfiz: 0! = 1 :-)
Stefano Zacchiroli [Wed, 12 Mar 2003 17:06:24 +0000 (17:06 +0000)]
- bugfiz: 0! = 1 :-)

21 years ago- reverted to >= dependencies for ocaml libraries
Stefano Zacchiroli [Wed, 12 Mar 2003 17:05:55 +0000 (17:05 +0000)]
- reverted to >= dependencies for ocaml libraries
- added build dep to graphviz

21 years agochanged interface of send_file function to enforce static type checking
Stefano Zacchiroli [Wed, 12 Mar 2003 17:05:22 +0000 (17:05 +0000)]
changed interface of send_file function to enforce static type checking
of its arguments

21 years ago* temporary fix for handling relative/absolute filenames in
Luca Padovani [Wed, 12 Mar 2003 15:51:55 +0000 (15:51 +0000)]
* temporary fix for handling relative/absolute filenames in
  the inclusion mechanisms of dictionaries

21 years ago* changed handling of ' (\primes) with a few patches in the stylesheets
Luca Padovani [Wed, 12 Mar 2003 10:18:02 +0000 (10:18 +0000)]
* changed handling of ' (\primes) with a few patches in the stylesheets

21 years agodebian release 0.4.1-1
Stefano Zacchiroli [Wed, 12 Mar 2003 02:06:59 +0000 (02:06 +0000)]
debian release 0.4.1-1

21 years agodebian release 0.0.4-1
Stefano Zacchiroli [Tue, 11 Mar 2003 11:34:30 +0000 (11:34 +0000)]
debian release 0.0.4-1

21 years agouse autotools also for ocaml part (again?)
Stefano Zacchiroli [Tue, 11 Mar 2003 11:33:56 +0000 (11:33 +0000)]
use autotools also for ocaml part (again?)

21 years ago- added support for NuPRL URIs in xml_url_of_uri
Stefano Zacchiroli [Tue, 25 Feb 2003 15:35:52 +0000 (15:35 +0000)]
- added support for NuPRL URIs in xml_url_of_uri
- added support for blank and #-commented lines in indexes
- added support for index lines terminated both with \r and \r\n

21 years ago- added default value for parse_patch function
Stefano Zacchiroli [Tue, 25 Feb 2003 14:13:39 +0000 (14:13 +0000)]
- added default value for parse_patch function
- reindented some tab

21 years agoadded is_blank_line facility to match line that should be ignored in
Stefano Zacchiroli [Tue, 25 Feb 2003 14:05:50 +0000 (14:05 +0000)]
added is_blank_line facility to match line that should be ignored in
indexes

21 years agoadded generation of DOT modules dependency graph
Stefano Zacchiroli [Tue, 25 Feb 2003 13:57:42 +0000 (13:57 +0000)]
added generation of DOT modules dependency graph

21 years agoAdded the special deletion. Pressing backspace, the user has a normal deletion
Paolo Marinelli [Mon, 24 Feb 2003 11:07:47 +0000 (11:07 +0000)]
Added the special deletion. Pressing backspace, the user has a normal deletion
(which can be either graphical or textual). Pressing backspace + alt, the user
has a special deletion (which can be either textual or graphical).
To implement this feature, all parser's methods concerning the deletion have
been modified: now, all of them have a boolean parameter, which indicates which
kind of deletion the method has to operate.
All methods' names have been changed: the word gdelete has been substitued with
drop.

21 years ago- better error messages on make failure
Stefano Zacchiroli [Sun, 23 Feb 2003 16:56:34 +0000 (16:56 +0000)]
- better error messages on make failure
- synced with O'Http 0.0.8

21 years agoadded hbugs-client META
Stefano Zacchiroli [Fri, 21 Feb 2003 13:56:04 +0000 (13:56 +0000)]
added hbugs-client META

21 years agorely on correct settings of OCAMLPATH
Stefano Zacchiroli [Fri, 21 Feb 2003 13:55:27 +0000 (13:55 +0000)]
rely on correct settings of OCAMLPATH

21 years agoadded pp for apply hint
Stefano Zacchiroli [Fri, 21 Feb 2003 13:47:43 +0000 (13:47 +0000)]
added pp for apply hint

21 years agorebuilt
Stefano Zacchiroli [Fri, 21 Feb 2003 13:46:59 +0000 (13:46 +0000)]
rebuilt

21 years ago* some fixes so to make Ocaml garbage collector happy
Luca Padovani [Fri, 21 Feb 2003 13:20:34 +0000 (13:20 +0000)]
* some fixes so to make Ocaml garbage collector happy
* there is still the problem that the assert macro is not recognized (?)

21 years ago* the minus sign is now mapped to the right Unicode character ant not
Luca Padovani [Fri, 21 Feb 2003 13:18:42 +0000 (13:18 +0000)]
* the minus sign is now mapped to the right Unicode character ant not
  to the dash -

21 years ago* removed debug message
Luca Padovani [Fri, 21 Feb 2003 13:18:10 +0000 (13:18 +0000)]
* removed debug message

21 years ago* click signal changed: now the element argument is optional
Luca Padovani [Fri, 21 Feb 2003 13:09:30 +0000 (13:09 +0000)]
* click signal changed: now the element argument is optional
  and if None it means the click was made on nothing. This is more
  uniform with the other signals

21 years agoglobal Makefile to build gTopLevel with all its dependencies
Stefano Zacchiroli [Thu, 20 Feb 2003 17:40:00 +0000 (17:40 +0000)]
global Makefile to build gTopLevel with all its dependencies

21 years agoexposed Http_message module
Stefano Zacchiroli [Thu, 20 Feb 2003 17:37:32 +0000 (17:37 +0000)]
exposed Http_message module

21 years agomoved here misc functions related to URIs from gTopLevel (they are
Stefano Zacchiroli [Thu, 20 Feb 2003 17:29:30 +0000 (17:29 +0000)]
moved here misc functions related to URIs from gTopLevel (they are
needed also outside gTopLevel)

21 years agoignore *.LOG files
Stefano Zacchiroli [Wed, 19 Feb 2003 14:23:44 +0000 (14:23 +0000)]
ignore *.LOG files

21 years agofirst tutors implementation, contains:
Stefano Zacchiroli [Wed, 19 Feb 2003 14:23:02 +0000 (14:23 +0000)]
first tutors implementation, contains:
- XML representation of available tutors
- scripts to list and start/stop available tutors
- script to generate simple tutors that simply use a tactic
- search_pattern_apply tutor

21 years ago- added run/'s .cvsignore ignoring *.LOG files
Stefano Zacchiroli [Wed, 19 Feb 2003 14:21:33 +0000 (14:21 +0000)]
- added run/'s .cvsignore ignoring *.LOG files

21 years ago- added distclean support
Stefano Zacchiroli [Wed, 19 Feb 2003 14:19:49 +0000 (14:19 +0000)]
- added distclean support
- added start/stop target to start/stop broker _and_ tutors
- added recursive invocation on meta and tutors dirs

21 years agorepresented new Wow message
Stefano Zacchiroli [Wed, 19 Feb 2003 14:18:43 +0000 (14:18 +0000)]
represented new Wow message

21 years ago- implemented status {,de}serialization
Stefano Zacchiroli [Wed, 19 Feb 2003 14:17:24 +0000 (14:17 +0000)]
- implemented status {,de}serialization
- implemented hint {,de}serialization
- added support for new Wow and Too_late messages
- added dump_msg debugging function
- added Unexpected_message exception

21 years ago- formalized proof engine status
Stefano Zacchiroli [Wed, 19 Feb 2003 14:04:17 +0000 (14:04 +0000)]
- formalized proof engine status
- formalized hints and hints list
- added Wow and Too_late broker -> tutor messages
- fixed Eureka message contents to carry a real life hint

21 years ago- added helm- modules dependencies
Stefano Zacchiroli [Wed, 19 Feb 2003 14:01:18 +0000 (14:01 +0000)]
- added helm- modules dependencies
- added ocamldoc generation of .dot modules dependency graph

21 years agorebuilt
Stefano Zacchiroli [Wed, 19 Feb 2003 14:00:20 +0000 (14:00 +0000)]
rebuilt

21 years agoadded common module
Stefano Zacchiroli [Wed, 19 Feb 2003 13:59:56 +0000 (13:59 +0000)]
added common module

21 years ago- added callbacks parameters to hbugsClient constructor (on_exit,
Stefano Zacchiroli [Wed, 19 Feb 2003 13:59:06 +0000 (13:59 +0000)]
- added callbacks parameters to hbugsClient constructor (on_exit,
  on_use_hint)
- hid methods used to handle local http daemon
- added and exposed methods registerToBroker, unregisterFromBroker,
  subscribeAll
- removed useHint, hint are returned on request by "hint" new method
- remeber availableTutors from last List_tutor message and use them to
  show tutors name instead of tutor id in main window
- handle double click on hint name to use an hint
- added wait parameter sendReq method to be able to wait the answer of
  a request
- added support for multiple hints received from broker
- clear old hints on state change
- subscribe to all available tutors on creation
- added subscribeSelected method

21 years ago- removed use hint button
Stefano Zacchiroli [Wed, 19 Feb 2003 13:51:26 +0000 (13:51 +0000)]
- removed use hint button
- rearragned subscribe part of main window

21 years agos/gui/hbugs_client_gui/
Stefano Zacchiroli [Wed, 19 Feb 2003 13:50:28 +0000 (13:50 +0000)]
s/gui/hbugs_client_gui/

21 years agofoo main program that instantiate a client GUI, for debugging purposes
Stefano Zacchiroli [Wed, 19 Feb 2003 13:49:41 +0000 (13:49 +0000)]
foo main program that instantiate a client GUI, for debugging purposes

21 years ago- bugfix: musings table is now consistent!
Stefano Zacchiroli [Wed, 19 Feb 2003 13:48:35 +0000 (13:48 +0000)]
- bugfix: musings table is now consistent!
- changed data structures used to hold musings: now explicitely use
  lists instead of relying on Hashtbl multiple bindings
- added isActive method on musings class

21 years ago- better specialization of some error messages
Stefano Zacchiroli [Wed, 19 Feb 2003 13:46:36 +0000 (13:46 +0000)]
- better specialization of some error messages
- added some informational messages
- use hint received from tutor instead of a fooish one
- control over answer from gTopLevel when sending hint
- commented out debugging wrapper which print all received messages

21 years ago- added doc target to generate .dot dependency graph using ocamldoc
Stefano Zacchiroli [Wed, 19 Feb 2003 13:38:17 +0000 (13:38 +0000)]
- added doc target to generate .dot dependency graph using ocamldoc
- added start/stop targets to start/stop broker
- clean run dir/ on distclean

21 years agoadded control script to start/stop broker
Stefano Zacchiroli [Wed, 19 Feb 2003 13:37:12 +0000 (13:37 +0000)]
added control script to start/stop broker

21 years agoadded hbugs-common and hbugs-thread_safe
Stefano Zacchiroli [Wed, 19 Feb 2003 13:36:28 +0000 (13:36 +0000)]
added hbugs-common and hbugs-thread_safe

21 years agoadded hbugs-common objects
Stefano Zacchiroli [Wed, 19 Feb 2003 13:35:54 +0000 (13:35 +0000)]
added hbugs-common objects

21 years agoadded META for hbugs client
Stefano Zacchiroli [Wed, 19 Feb 2003 13:34:55 +0000 (13:34 +0000)]
added META for hbugs client

21 years ago* the stylesheet does not generate the tml namespace anymore
Luca Padovani [Fri, 14 Feb 2003 15:15:05 +0000 (15:15 +0000)]
* the stylesheet does not generate the tml namespace anymore

21 years ago* removed memory leak (maybe)
Luca Padovani [Fri, 14 Feb 2003 15:10:30 +0000 (15:10 +0000)]
* removed memory leak (maybe)
* used Val_Element_ref instead of reffing explicitly

21 years agoDebug code removed.
Claudio Sacerdoti Coen [Fri, 14 Feb 2003 11:58:17 +0000 (11:58 +0000)]
Debug code removed.

21 years ago* assertion too strict removed
Luca Padovani [Thu, 13 Feb 2003 13:22:00 +0000 (13:22 +0000)]
* assertion too strict removed

21 years ago* added missing dependencies
Luca Padovani [Thu, 13 Feb 2003 13:20:40 +0000 (13:20 +0000)]
* added missing dependencies

21 years agoType fixed.
Claudio Sacerdoti Coen [Thu, 13 Feb 2003 12:51:08 +0000 (12:51 +0000)]
Type fixed.

21 years ago* added show/hide cursro methods
Luca Padovani [Thu, 13 Feb 2003 12:40:34 +0000 (12:40 +0000)]
* added show/hide cursro methods
* some code cleanup
* fix in reset
* fix in get_tex (binding ocaml)
* added tex to mml translator

21 years ago* the type of the constructor was wrong
Luca Padovani [Wed, 12 Feb 2003 16:24:58 +0000 (16:24 +0000)]
* the type of the constructor was wrong

21 years ago* bind of method get_drawing_area
Luca Padovani [Wed, 12 Feb 2003 13:08:21 +0000 (13:08 +0000)]
* bind of method get_drawing_area
* currently the test doesn't do anything with it

21 years agoBug fixed. In the previous version, all right open macros and all delimited arguments
Paolo Marinelli [Wed, 12 Feb 2003 09:16:56 +0000 (09:16 +0000)]
Bug fixed. In the previous version, all right open macros and all delimited arguments
of a macro, could be closed inserting a closing brace.
Now, a right open macro can be closed only if it's contained in a group (with id).
To close it, the user has to type a closing brace, which closes the group.
A right open macro not contained in a group, cannot be closed: any closing brace
is ignored.
The only way to exit from a delimited argument, the user has to type the delimiter (or the
sequence of delimiters).
To fix this bug, a new method has been added to the TPushParser class. This method
(bool correctBrace(void)), is used to determine if a closing brace is appropriate to
close a right open macro.
In addition, advance method has been modified.

21 years ago* this is a large commit
Luca Padovani [Sat, 8 Feb 2003 22:13:29 +0000 (22:13 +0000)]
* this is a large commit
* added freeze/thaw methods to parser
* added XSLT + Diff class
* added <include> method for including dictionaries
* added preliminary ocaml binding (C+ML)
* code cleanup

21 years ago* added apply method that takes no parameters
Luca Padovani [Sat, 8 Feb 2003 22:09:57 +0000 (22:09 +0000)]
* added apply method that takes no parameters

21 years agoAdded support for NuPRL URIs.
Claudio Sacerdoti Coen [Fri, 7 Feb 2003 12:05:57 +0000 (12:05 +0000)]
Added support for NuPRL URIs.

Note: theory files are supported only for CIC. To be understood.

21 years agoAdded some controls to handle the case in which the user type an unexpected '{'
Paolo Marinelli [Thu, 6 Feb 2003 11:53:48 +0000 (11:53 +0000)]
Added some controls to handle the case in which the user type an unexpected '{'
character. Now, the editor doesn't crash, but emit an error.
Removed some debug messages.

21 years agoMakefile.common.in and .depend backtracked to my last commit (before the
Claudio Sacerdoti Coen [Wed, 5 Feb 2003 12:46:20 +0000 (12:46 +0000)]
Makefile.common.in and .depend backtracked to my last commit (before the
ones of Ferruccio) and then modified. Dependencies between a file and a
library are now handled correctly.

21 years agopackege dependences calculation patched
Ferruccio Guidi [Wed, 5 Feb 2003 11:42:52 +0000 (11:42 +0000)]
packege dependences calculation patched

21 years agoMissing parameters added to MathML Content mode.
Claudio Sacerdoti Coen [Wed, 5 Feb 2003 11:28:41 +0000 (11:28 +0000)]
Missing parameters added to MathML Content mode.

21 years agopackage dependences calulation fixed
Ferruccio Guidi [Wed, 5 Feb 2003 11:09:48 +0000 (11:09 +0000)]
package dependences calulation fixed

21 years agoSQL quoting fixed in relation.ml
Ferruccio Guidi [Tue, 4 Feb 2003 19:08:28 +0000 (19:08 +0000)]
SQL quoting fixed in relation.ml

21 years agoAdded some controls for the graphical deleting of apostrophe.
Paolo Marinelli [Tue, 4 Feb 2003 16:21:10 +0000 (16:21 +0000)]
Added some controls for the graphical deleting of apostrophe.
The code for the graphical deleting is now divided in several private methods, which
 make the code clearer.
Partially added the use of the logger in the class TPushParser.
Some little errors has been eliminated in the implementation of the class
TPushParser.

21 years agoprint_endline ==> prerr_endline
Claudio Sacerdoti Coen [Tue, 4 Feb 2003 12:17:02 +0000 (12:17 +0000)]
print_endline ==> prerr_endline
and other minor code improvements

21 years agoBug fixed: ' must be quoted.
Claudio Sacerdoti Coen [Tue, 4 Feb 2003 12:15:15 +0000 (12:15 +0000)]
Bug fixed: ' must be quoted.

21 years agoBug fixed: "'" must be quoted.
Claudio Sacerdoti Coen [Tue, 4 Feb 2003 12:14:03 +0000 (12:14 +0000)]
Bug fixed: "'" must be quoted.

21 years agoold file removed
Ferruccio Guidi [Mon, 3 Feb 2003 21:19:35 +0000 (21:19 +0000)]
old file removed