]>
 
 
matita.cs.unibo.it Git - helm.git/log 
 
 
 
 
 
 
Stefano Zacchiroli  [Thu, 19 Jun 2003 15:27:32 +0000  (15:27 +0000)] 
 
debian version 0.0.4-5 
 
Claudio Sacerdoti Coen  [Thu, 19 Jun 2003 15:25:33 +0000  (15:25 +0000)] 
 
New version 0.0.2: 
 
* Bug fixed: 
  - the *PushLexer reset method did not notify the PushParser of the 
    buffer reset 
  - the reset() method of the ocaml binding did not reset the Lexer. 
    Closes #85 and #86 
  - Even if the cursor is not visible, its value should be rendered 
    in MathML Presentation and it should be printed in TeX. Fixed 
    both xml-mmlp.xsl and tml-tex.xsl 
 
* New stuff: 
  - the LPushLexer now recognized \/ as a long identifier character. 
  - Added a new tml-litex.xsl stylesheet from TML to TeX + long identifiers. 
    It should be (but it is not yet) the inverse function of the 
    parser 
 
Luca Padovani  [Thu, 19 Jun 2003 15:11:38 +0000  (15:11 +0000)] 
 
* added pkg-config stuff 
 
Stefano Zacchiroli  [Thu, 19 Jun 2003 15:00:50 +0000  (15:00 +0000)] 
 
fixed autoconf variable @@ vs $() 
 
Ferruccio Guidi  [Thu, 19 Jun 2003 14:37:12 +0000  (14:37 +0000)] 
 
MathQL 1.3 ready for use 
 
Stefano Zacchiroli  [Thu, 19 Jun 2003 14:30:24 +0000  (14:30 +0000)] 
 
debian version 0.4.3 (maybe, not tested) 
 
Luca Padovani  [Thu, 19 Jun 2003 13:11:30 +0000  (13:11 +0000)] 
 
* removed *-config script invocations, now using pkg-config 
 
Stefano Zacchiroli  [Thu, 19 Jun 2003 13:01:37 +0000  (13:01 +0000)] 
 
bumped version to 0.4.3 
 
Claudio Sacerdoti Coen  [Wed, 18 Jun 2003 12:55:21 +0000  (12:55 +0000)] 
 
No longer used. 
 
Luca Padovani  [Wed, 18 Jun 2003 12:53:24 +0000  (12:53 +0000)] 
 
* added template for tml:s 
* if the cursor is the empty string it is not produced 
 
Claudio Sacerdoti Coen  [Tue, 10 Jun 2003 14:59:38 +0000  (14:59 +0000)] 
 
- tabs removed 
- "\" correctly quoted in strings 
- in case of self-loops, the process diverged. Self-loops are now 
  ignored during parsing. 
 
Claudio Sacerdoti Coen  [Tue, 10 Jun 2003 14:44:39 +0000  (14:44 +0000)] 
 
findlib introduced 
 
Luca Padovani  [Wed, 4 Jun 2003 13:00:55 +0000  (13:00 +0000)] 
 
* the non-empty cursor is now generated 
 
Luca Padovani  [Wed, 4 Jun 2003 10:50:10 +0000  (10:50 +0000)] 
 
* patched wrong commit (perhaps...) 
 
Ferruccio Guidi  [Sat, 31 May 2003 18:59:06 +0000  (18:59 +0000)] 
 
new syntax for "property" enabled: 
 now many "isfalse" clauses are accepted 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 17:17:58 +0000  (17:17 +0000)] 
 
final ispell 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 17:13:42 +0000  (17:13 +0000)] 
 
Minor modifications to the new session. 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 15:20:28 +0000  (15:20 +0000)] 
 
... 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 15:18:31 +0000  (15:18 +0000)] 
 
... 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 15:18:26 +0000  (15:18 +0000)] 
 
color ==> gray 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 15:09:45 +0000  (15:09 +0000)] 
 
... 
 
Claudio Sacerdoti Coen  [Fri, 30 May 2003 15:08:25 +0000  (15:08 +0000)] 
 
New session (the H-Bugs interactive session). 
 
Stefano Zacchiroli  [Thu, 29 May 2003 21:14:06 +0000  (21:14 +0000)] 
 
draft review 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 20:52:06 +0000  (20:52 +0000)] 
 
New ispell. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 20:48:45 +0000  (20:48 +0000)] 
 
Several other small changes here and there. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 17:59:37 +0000  (17:59 +0000)] 
 
... 
 
Stefano Zacchiroli  [Thu, 29 May 2003 17:57:06 +0000  (17:57 +0000)] 
 
thread handling reviewed 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 17:50:52 +0000  (17:50 +0000)] 
 
Figure moved to the next page. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 17:48:22 +0000  (17:48 +0000)] 
 
Several editor notes resolved. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 13:43:15 +0000  (13:43 +0000)] 
 
Everything Ispell-ed. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 13:31:42 +0000  (13:31 +0000)] 
 
Other references added. 
An old part removed. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 12:26:57 +0000  (12:26 +0000)] 
 
A new references. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 12:22:28 +0000  (12:22 +0000)] 
 
Many references committed. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 11:34:30 +0000  (11:34 +0000)] 
 
Some editor notes closed. 
 
Claudio Sacerdoti Coen  [Thu, 29 May 2003 11:29:39 +0000  (11:29 +0000)] 
 
Lots of small changes in the text. 
 
Ferruccio Guidi  [Wed, 28 May 2003 13:57:33 +0000  (13:57 +0000)] 
 
extended syntax for add 
 
Claudio Sacerdoti Coen  [Wed, 28 May 2003 12:01:43 +0000  (12:01 +0000)] 
 
- several changes in all the parts that made comparisons with MONET 
- added a few sentences in the conclusions section 
 
Stefano Zacchiroli  [Wed, 28 May 2003 06:58:59 +0000  (06:58 +0000)] 
 
added web-services' interfaces image 
 
Stefano Zacchiroli  [Wed, 28 May 2003 06:58:47 +0000  (06:58 +0000)] 
 
- reviewed latest CSC'comments 
- added future works 
- added an image 
 
Ferruccio Guidi  [Tue, 27 May 2003 13:24:52 +0000  (13:24 +0000)] 
 
site updated 
 
Claudio Sacerdoti Coen  [Tue, 27 May 2003 13:11:44 +0000  (13:11 +0000)] 
 
Several small changes to the parts committed by Zack. 
 
Stefano Zacchiroli  [Mon, 26 May 2003 12:44:47 +0000  (12:44 +0000)] 
 
added status.eps 
 
Stefano Zacchiroli  [Mon, 26 May 2003 07:53:49 +0000  (07:53 +0000)] 
 
written section 3 
 
Claudio Sacerdoti Coen  [Fri, 23 May 2003 11:50:12 +0000  (11:50 +0000)] 
 
First part of the chapter about tutors. The automatic generation part is 
still missing. 
 
Stefano Zacchiroli  [Fri, 23 May 2003 11:11:42 +0000  (11:11 +0000)] 
 
- (badly) written section 2 (Architecture) 
- removed old oldparts in introduction, added some ednotes 
 
Stefano Zacchiroli  [Fri, 23 May 2003 11:09:54 +0000  (11:09 +0000)] 
 
added architecture figure 
 
Stefano Zacchiroli  [Fri, 23 May 2003 11:05:03 +0000  (11:05 +0000)] 
 
added MONET's Math Obj Manager to conclusions 
 
Stefano Zacchiroli  [Fri, 23 May 2003 11:04:31 +0000  (11:04 +0000)] 
 
added multiple invocations of latex 
 
Claudio Sacerdoti Coen  [Fri, 23 May 2003 09:56:15 +0000  (09:56 +0000)] 
 
Added all (???) the sections and their labels. 
 
Claudio Sacerdoti Coen  [Fri, 23 May 2003 09:52:48 +0000  (09:52 +0000)] 
 
Minor improvements in the introduction. 
 
Luca Padovani  [Fri, 23 May 2003 09:24:55 +0000  (09:24 +0000)] 
 
* fix in optional argument for ocaml binding 
* fix in tml->mmlp stylehseet 
 
Claudio Sacerdoti Coen  [Thu, 22 May 2003 17:51:48 +0000  (17:51 +0000)] 
 
- Introduction changed. 
- Tasks assigned. 
 
Claudio Sacerdoti Coen  [Thu, 22 May 2003 16:05:12 +0000  (16:05 +0000)] 
 
ed and draftstamp packages committed and activated 
 
Ferruccio Guidi  [Thu, 22 May 2003 14:49:52 +0000  (14:49 +0000)] 
 
mathql query generator interface patched 
 
Stefano Zacchiroli  [Thu, 22 May 2003 07:33:44 +0000  (07:33 +0000)] 
 
first checkin 
- introduction 
- outline 
- auxiliary files 
 
Ferruccio Guidi  [Wed, 21 May 2003 11:00:31 +0000  (11:00 +0000)] 
 
patched 
 
Ferruccio Guidi  [Tue, 20 May 2003 14:52:11 +0000  (14:52 +0000)] 
 
MathQL query generator: new interface 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 16:51:37 +0000  (16:51 +0000)] 
 
Several changes: 
 
1. the UWOBO_LOG_FILE environment variable semantics changed. It is now 
   used in the following way: $UWOBO_LOG_FILE.pid.log 
2. when the log file can not be opened, UWOBO used to crash. Instead, 
   it now goes on and a nice error message is printed on the stderr 
   (but, unfortunately, it is not given back to the user, since the 
   error is raised in a new process and it can not be read back from 
   the logfile!) 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 16:31:05 +0000  (16:31 +0000)] 
 
The semantics of the UWOBO_LOG variable has changed: the suffix ".log" 
should not be in there any more. 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 16:30:38 +0000  (16:30 +0000)] 
 
The chmod ug+w in the all rule has been made non-critical. 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 12:18:30 +0000  (12:18 +0000)] 
 
This commit undoes part of the previous commit, where I mistakenly committed 
parts of my laptop settings. 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 12:15:43 +0000  (12:15 +0000)] 
 
New: two methods have been added to kill UWOBO and to start a new session 
     (i.e. a new UWOBO process) listening on a given port) 
 
Claudio Sacerdoti Coen  [Thu, 15 May 2003 12:11:52 +0000  (12:11 +0000)] 
 
New: two new methods added 
 
* /newsession to create a new session on a given port (i.e. to fork a new 
  UWOBO that starts listening on the new given port) 
* /kill to ask an UWOBO to finish the execution 
 
Ferruccio Guidi  [Wed, 30 Apr 2003 13:56:57 +0000  (13:56 +0000)] 
 
MQueryInterpreter: interface updated 
 
Claudio Sacerdoti Coen  [Tue, 29 Apr 2003 16:16:02 +0000  (16:16 +0000)] 
 
New dependencies. 
 
Claudio Sacerdoti Coen  [Tue, 29 Apr 2003 16:14:25 +0000  (16:14 +0000)] 
 
New: stylesheets are now partially cached (i.e. all the stylesheets which 
are applied using an empty list of props are now precompiled only when 
added or reloaded). See bug #75. 
 
Claudio Sacerdoti Coen  [Mon, 28 Apr 2003 17:45:58 +0000  (17:45 +0000)] 
 
No more used since a long time. 
 
Claudio Sacerdoti Coen  [Mon, 28 Apr 2003 17:16:46 +0000  (17:16 +0000)] 
 
When the stylesheet from TML to MathML generated a document without a root 
an assertion failed. The new implementation creates an empty document 
(with only a m:math root element) and prints an error message (using the 
logger). 
 
Claudio Sacerdoti Coen  [Mon, 28 Apr 2003 17:15:18 +0000  (17:15 +0000)] 
 
The stylesheet used to generate an empty (and not even well-formed) XML document 
when given a document whose root element is tml:tex and whose only child 
is a non-visible cursor. The problem is fixed generating a <m:math/> document 
(ignoring the visibility status of the cursor). 
 
Claudio Sacerdoti Coen  [Mon, 28 Apr 2003 17:13:39 +0000  (17:13 +0000)] 
 
The reset() method ignored the fact that the widget can be frozen. Fixed. 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 16:47:55 +0000  (16:47 +0000)] 
 
patch 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 15:15:18 +0000  (15:15 +0000)] 
 
patch 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 15:10:42 +0000  (15:10 +0000)] 
 
patch 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 12:35:39 +0000  (12:35 +0000)] 
 
patch 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 12:03:07 +0000  (12:03 +0000)] 
 
patch 
 
Ferruccio Guidi  [Wed, 23 Apr 2003 11:05:32 +0000  (11:05 +0000)] 
 
- New interface for the MathQL interpreter (1.3 version) 
- Two toplevels committed in ocaml/mathql_test (new directory) 
 
Claudio Sacerdoti Coen  [Tue, 22 Apr 2003 10:17:38 +0000  (10:17 +0000)] 
 
Improved exception catching. 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 15:41:30 +0000  (15:41 +0000)] 
 
bugfix: print a better exception than "Not_found" when "baseuri" 
parameter for "ls" method is empty or simply unparsable 
 
Claudio Sacerdoti Coen  [Wed, 16 Apr 2003 14:14:45 +0000  (14:14 +0000)] 
 
- removed unclear parameter on_exit 
- renamed on_use_hint to use_hint_callback 
- added method setUseHintCallback 
 
Claudio Sacerdoti Coen  [Wed, 16 Apr 2003 14:12:30 +0000  (14:12 +0000)] 
 
Use of Hbugs_deity for thread creation and killing. 
 
Claudio Sacerdoti Coen  [Wed, 16 Apr 2003 14:11:28 +0000  (14:11 +0000)] 
 
Support for optional state (empty XML element). 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 12:51:25 +0000  (12:51 +0000)] 
 
- use an exception to handle empty status nodes 
- removed some ancient comments 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 12:49:35 +0000  (12:49 +0000)] 
 
updated serialization test 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 12:16:27 +0000  (12:16 +0000)] 
 
no longer used (use HBUGS_MESSAGES.xml directly) 
 
Claudio Sacerdoti Coen  [Wed, 16 Apr 2003 12:04:35 +0000  (12:04 +0000)] 
 
- support None state 
- added (de)serialization of Too_late 
 
Claudio Sacerdoti Coen  [Wed, 16 Apr 2003 12:04:12 +0000  (12:04 +0000)] 
 
State_change can now contain a state of None indicating that the proof 
is completed 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 11:44:28 +0000  (11:44 +0000)] 
 
added "restart" target 
 
Stefano Zacchiroli  [Wed, 16 Apr 2003 10:05:09 +0000  (10:05 +0000)] 
 
added ocamlfind trick to trigger rebuild when some library's .cma has 
been changed 
 
Stefano Zacchiroli  [Tue, 15 Apr 2003 15:47:42 +0000  (15:47 +0000)] 
 
added support for slaves killing 
 
Claudio Sacerdoti Coen  [Thu, 10 Apr 2003 17:11:46 +0000  (17:11 +0000)] 
 
NuPrlDefinition element handling added 
 
Claudio Sacerdoti Coen  [Thu, 10 Apr 2003 17:05:40 +0000  (17:05 +0000)] 
 
extra_info hack removed 
 
Claudio Sacerdoti Coen  [Thu, 10 Apr 2003 17:04:01 +0000  (17:04 +0000)] 
 
@uri attribute added to tacticinstance. A "Tactic details" hyperlink is 
now automatically generated starting from it. 
 
Claudio Sacerdoti Coen  [Thu, 10 Apr 2003 17:03:29 +0000  (17:03 +0000)] 
 
The UNICODEvsSYMBOL machinery is now working again. 
 
Claudio Sacerdoti Coen  [Tue, 8 Apr 2003 15:16:45 +0000  (15:16 +0000)] 
 
nuprl_content_to_html.xsl is not used. Let's definitely remove it. 
 
Claudio Sacerdoti Coen  [Tue, 8 Apr 2003 14:44:51 +0000  (14:44 +0000)] 
 
First commit of the NuPRL stylesheets. 
 
Stefano Zacchiroli  [Tue, 8 Apr 2003 08:21:20 +0000  (08:21 +0000)] 
 
kill instances of uwobo_forever.sh on stop 
 
Stefano Zacchiroli  [Tue, 8 Apr 2003 08:12:43 +0000  (08:12 +0000)] 
 
- added support for UWOBO respawner 
- added some newline related pretty printing 
 
Stefano Zacchiroli  [Tue, 8 Apr 2003 08:12:17 +0000  (08:12 +0000)] 
 
added UWOBO respawner script 
 
Stefano Zacchiroli  [Mon, 7 Apr 2003 16:26:03 +0000  (16:26 +0000)] 
 
getter's panel check in 
 
Stefano Zacchiroli  [Mon, 7 Apr 2003 16:06:12 +0000  (16:06 +0000)] 
 
added a TODO bug comment