]>
matita.cs.unibo.it Git - helm.git/log
Luca Padovani [Sat, 4 Oct 2003 08:21:57 +0000 (08:21 +0000)]
* changed version in configure.ac
* gdome_xslt.c renamed into x_gdome_xslt.c otherwise there was a conflict
with make rules that prevented gdome_xslt.o from being built correctly
Luca Padovani [Fri, 3 Oct 2003 14:14:51 +0000 (14:14 +0000)]
* further code cleanup
Luca Padovani [Fri, 3 Oct 2003 14:03:15 +0000 (14:03 +0000)]
* updated #include directives
* clean up of some makefiles
Andrea Asperti [Wed, 1 Oct 2003 13:08:08 +0000 (13:08 +0000)]
* the main function MUST return 0 to communicate everything was OK
Andrea Asperti [Wed, 1 Oct 2003 08:39:17 +0000 (08:39 +0000)]
* new version of metadata extraction
* metadata are inserted directly without creating the RDF document
Luca Padovani [Fri, 26 Sep 2003 15:55:54 +0000 (15:55 +0000)]
* the regular expressions must have $ otherwise the shortest match
will be found first and the annotations will never show up
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:41:25 +0000 (17:41 +0000)]
...
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:40:08 +0000 (17:40 +0000)]
Reindentation.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:39:01 +0000 (17:39 +0000)]
ProofEngine.goal := ==> set_proof_engine_goal
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:33:30 +0000 (17:33 +0000)]
Reindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 17:25:28 +0000 (17:25 +0000)]
ProofEngine.proof is now an abstract data type (since we plan to have OMDoc
in the future as the persistent format).
Ferruccio Guidi [Tue, 23 Sep 2003 17:06:50 +0000 (17:06 +0000)]
patch
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 16:10:16 +0000 (16:10 +0000)]
This version of xmlDiff is much much much smarter than the previous one:
with the forthcoming version of gdome the performances will be doubled.
[ Unfortunately, it is still deadly slow. ]
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:58:28 +0000 (15:58 +0000)]
Reindentation
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:56:42 +0000 (15:56 +0000)]
BU_Conversion + omit-conclusion is a mess. I have partially fixed the
problem by ignoring the omit-conclusion flag.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 15:55:28 +0000 (15:55 +0000)]
Debugging stuff removed.
Ferruccio Guidi [Tue, 23 Sep 2003 15:12:46 +0000 (15:12 +0000)]
Now mathql_generator compiles before mathql_interpreter.
This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 12:06:54 +0000 (12:06 +0000)]
Preliminary support for proof-tree enhanced: proof-trees are now shown
as views over .con files.
Claudio Sacerdoti Coen [Tue, 23 Sep 2003 11:12:38 +0000 (11:12 +0000)]
- added support for proof trees
- fixed typo in body.ann regexp
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 13:00:28 +0000 (13:00 +0000)]
clean_cache method added
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:57:01 +0000 (12:57 +0000)]
cleancache ==> clean_cache
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 12:44:51 +0000 (12:44 +0000)]
Clean cache method added.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 11:58:43 +0000 (11:58 +0000)]
param.framewidth = 150 (hard-coded ;-( pour Hanane ;-((((((((((
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 11:33:47 +0000 (11:33 +0000)]
Following an hyperlink from a proof-tree rendering now brings you to
the lambda-term rendering of the proof statement.
Claudio Sacerdoti Coen [Fri, 19 Sep 2003 08:10:14 +0000 (08:10 +0000)]
Preliminary commit to support Hanane's proof-tree rendering.
Claudio Sacerdoti Coen [Thu, 18 Sep 2003 15:41:11 +0000 (15:41 +0000)]
prop.media-type and prop.encoding were _NOT_ considered when the
corresponding HTML <meta/> was generated. Fixed.
Claudio Sacerdoti Coen [Wed, 17 Sep 2003 12:27:50 +0000 (12:27 +0000)]
www-sop.inria.fr
^
Hyphen in the name of the server were not allowed. Fixed.
Stefano Zacchiroli [Sun, 14 Sep 2003 00:03:18 +0000 (00:03 +0000)]
- bumped copyright years
- added support for proof checker environment dump/save/restore
- added support for hbugs notify upon goal change (disabled by default)
- added (re)submit option to hbugs menu
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:34 +0000 (00:01 +0000)]
- converted TAB to spaces
Stefano Zacchiroli [Sun, 14 Sep 2003 00:01:25 +0000 (00:01 +0000)]
- clear hints list upon status submit
- converted TAB to spaces
Stefano Zacchiroli [Sat, 13 Sep 2003 23:59:22 +0000 (23:59 +0000)]
- added support for dumping environment to file on exit (disabled by default)
- added environment restore on boot
Stefano Zacchiroli [Sat, 13 Sep 2003 23:58:39 +0000 (23:58 +0000)]
added environment setting (set by fill_template)
Stefano Zacchiroli [Sat, 13 Sep 2003 23:58:01 +0000 (23:58 +0000)]
added environment file setting for each tutor
Stefano Zacchiroli [Sat, 13 Sep 2003 23:57:23 +0000 (23:57 +0000)]
added support for dump/restore/clear proof checker cache
Stefano Zacchiroli [Sat, 13 Sep 2003 23:56:42 +0000 (23:56 +0000)]
added notation for reals 0, 1, n
Luca Padovani [Sat, 13 Sep 2003 15:36:27 +0000 (15:36 +0000)]
* small fixes for distribution
Luca Padovani [Sat, 13 Sep 2003 15:22:13 +0000 (15:22 +0000)]
* fixed dependency on gtkmathview 0.5.1
Luca Padovani [Sat, 13 Sep 2003 15:20:49 +0000 (15:20 +0000)]
* added licence to IDL file
Luca Padovani [Sat, 13 Sep 2003 15:20:22 +0000 (15:20 +0000)]
* some code cleanup
* added LICENCE to all source files
Luca Padovani [Fri, 12 Sep 2003 10:20:14 +0000 (10:20 +0000)]
* using the clipboard to communicate the id of the selected subtree
Luca Padovani [Wed, 10 Sep 2003 07:55:33 +0000 (07:55 +0000)]
* completed implementation of View interface
Luca Padovani [Tue, 9 Sep 2003 20:18:39 +0000 (20:18 +0000)]
* prototypes for auxiliary C++ functions
Luca Padovani [Tue, 9 Sep 2003 20:17:50 +0000 (20:17 +0000)]
* advanced implementation of View interface
pmasoudi [Tue, 9 Sep 2003 16:21:25 +0000 (16:21 +0000)]
snapshot
Luca Padovani [Tue, 9 Sep 2003 13:42:40 +0000 (13:42 +0000)]
* snapshot
Luca Padovani [Tue, 9 Sep 2003 07:35:15 +0000 (07:35 +0000)]
* exceptionset -> exception_set
Luca Padovani [Mon, 8 Sep 2003 20:09:07 +0000 (20:09 +0000)]
* update
Luca Padovani [Mon, 8 Sep 2003 20:07:34 +0000 (20:07 +0000)]
* code cleanup
* added partial implementation for view
Luca Padovani [Mon, 8 Sep 2003 19:59:22 +0000 (19:59 +0000)]
* IDL file update (and renamed)
pmasoudi [Mon, 8 Sep 2003 15:04:22 +0000 (15:04 +0000)]
select and click signal added
Ferruccio Guidi [Mon, 8 Sep 2003 11:57:43 +0000 (11:57 +0000)]
added information on the "qdl" article with C.S.C.
Stefano Zacchiroli [Sun, 7 Sep 2003 09:53:48 +0000 (09:53 +0000)]
use an integer debugging level instead of a boolean one
Stefano Zacchiroli [Sun, 7 Sep 2003 09:53:03 +0000 (09:53 +0000)]
- use hbugs' describe_callback to render apply-hints on selection
- sync default uri proposed while loading a new proof and loading one
- resend status to hbugs on tab change
Stefano Zacchiroli [Sun, 7 Sep 2003 09:50:58 +0000 (09:50 +0000)]
commented out gtkmathview's font_size override
Stefano Zacchiroli [Sun, 7 Sep 2003 09:50:29 +0000 (09:50 +0000)]
added "start" and "stop" targets for hbugs
Stefano Zacchiroli [Sun, 7 Sep 2003 09:50:09 +0000 (09:50 +0000)]
added support for external configuration of describe_hint_callback
Stefano Zacchiroli [Sun, 7 Sep 2003 09:49:07 +0000 (09:49 +0000)]
added "describe_hint_callback" invoked when a hint is selected
Stefano Zacchiroli [Sun, 7 Sep 2003 09:48:27 +0000 (09:48 +0000)]
- removed useless status bar
- hid menu bar
- added (Re)Register button
- added vertical pane between subscription and hints
- changed default size to a "decent"-one
Stefano Zacchiroli [Sun, 7 Sep 2003 09:47:03 +0000 (09:47 +0000)]
send SIGKILL to stop web services
Stefano Zacchiroli [Sun, 7 Sep 2003 09:46:14 +0000 (09:46 +0000)]
commented out thread killing (we have to wait for a decent Thread.exit
implementation)
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 17:33:04 +0000 (17:33 +0000)]
get_childNodes no longer used ==> major performance speed-up
Stefano Zacchiroli [Fri, 5 Sep 2003 16:23:17 +0000 (16:23 +0000)]
Defs in context may now have an optional type (when unknown).
During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.
Stefano Zacchiroli [Fri, 5 Sep 2003 16:22:09 +0000 (16:22 +0000)]
added \neqt macro
Stefano Zacchiroli [Fri, 5 Sep 2003 16:18:53 +0000 (16:18 +0000)]
added notation for Ropp and Rinv
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 15:39:28 +0000 (15:39 +0000)]
string ==> id
Stefano Zacchiroli [Fri, 5 Sep 2003 15:36:28 +0000 (15:36 +0000)]
Defs in context may now have an optional type (when unknown).
During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.
Stefano Zacchiroli [Fri, 5 Sep 2003 15:34:43 +0000 (15:34 +0000)]
fixed associativity of some (all!) binary operators
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 14:31:16 +0000 (14:31 +0000)]
Replace is now working also over Type.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 13:00:27 +0000 (13:00 +0000)]
Replace tactic fixed. It was not working any longer. (It produced a dummy
eta-expansion).
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 12:34:07 +0000 (12:34 +0000)]
Notation for Rdiv and Rminus.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:59:02 +0000 (10:59 +0000)]
Debugging infos removed.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:29:52 +0000 (10:29 +0000)]
string => id
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:29:13 +0000 (10:29 +0000)]
Defs in context may now have an optional type (when unknown).
During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.
Stefano Zacchiroli [Fri, 5 Sep 2003 08:51:56 +0000 (08:51 +0000)]
replaced with my generic latex makefile
Luca Padovani [Thu, 4 Sep 2003 19:32:38 +0000 (19:32 +0000)]
* update with some candidate methods
Luca Padovani [Thu, 4 Sep 2003 18:46:14 +0000 (18:46 +0000)]
* added test View interface. It is basically empty but eventually it will host
any gtkmathview-specific method
Stefano Zacchiroli [Thu, 4 Sep 2003 16:46:46 +0000 (16:46 +0000)]
- added a destroy callback
- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_
Stefano Zacchiroli [Thu, 4 Sep 2003 16:46:03 +0000 (16:46 +0000)]
start tutors with nice at the lowest priority
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:44 +0000 (16:45 +0000)]
avoid deletion of useful .cmi with .PRECIOUS
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:25 +0000 (16:45 +0000)]
commented out debugging tutor "wait"
Stefano Zacchiroli [Thu, 4 Sep 2003 16:44:04 +0000 (16:44 +0000)]
- added dot notation for real numbers and basic operations on them
- added support for \eqt
Stefano Zacchiroli [Thu, 4 Sep 2003 16:43:25 +0000 (16:43 +0000)]
- added default URI for new theorems
- added menu items to the hbugs menu for:
* start and stop hbugs web services
* force submission of current status
Stefano Zacchiroli [Thu, 4 Sep 2003 16:42:13 +0000 (16:42 +0000)]
added support for X11 clipboard pasting with CTRL-V shortcut
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:38 +0000 (16:41 +0000)]
added methods to start/stop web services
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:14 +0000 (16:41 +0000)]
added eqT's macro
pmasoudi [Thu, 4 Sep 2003 15:05:48 +0000 (15:05 +0000)]
scrollbars added & control structure screated
Stefano Zacchiroli [Thu, 4 Sep 2003 15:02:03 +0000 (15:02 +0000)]
fixed typo in eqT's URI
Ferruccio Guidi [Thu, 4 Sep 2003 13:07:26 +0000 (13:07 +0000)]
CGLocateInductive patched
Ferruccio Guidi [Thu, 4 Sep 2003 11:04:15 +0000 (11:04 +0000)]
added the support for the "Locate Inductive Principles" query
Luca Padovani [Fri, 1 Aug 2003 15:32:17 +0000 (15:32 +0000)]
* removed wrong unref
Luca Padovani [Fri, 1 Aug 2003 10:31:22 +0000 (10:31 +0000)]
* added test .html file for mozilla plugin
Luca Padovani [Fri, 1 Aug 2003 10:15:57 +0000 (10:15 +0000)]
* a few adjustments and debugging messages added
* works as a component in mozilla
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 15:41:05 +0000 (15:41 +0000)]
Closed induction cases are now pointers to the acontext/conclusion ==>
they are now perforated correctly.
pmasoudi [Thu, 31 Jul 2003 14:54:14 +0000 (14:54 +0000)]
* added first version of persist stream implementation (not yet working)
* added test for property bag (read-only for now)
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 14:44:25 +0000 (14:44 +0000)]
"proof of X" closed mactions were not selectable
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 08:14:43 +0000 (08:14 +0000)]
1. folded maction are now selectable
2. metavariable occurrences are now displayed together with their
substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order
Luca Padovani [Wed, 30 Jul 2003 17:45:58 +0000 (17:45 +0000)]
* mime type updated
Ferruccio Guidi [Wed, 30 Jul 2003 15:45:03 +0000 (15:45 +0000)]
- support for comments added in mathql_db_map.txt
Claudio Sacerdoti Coen [Wed, 30 Jul 2003 15:43:30 +0000 (15:43 +0000)]
Unuseful id removed from hypothesis.
Ferruccio Guidi [Wed, 30 Jul 2003 15:29:52 +0000 (15:29 +0000)]
- information about the database map added in whatsnew.html
- spell checked