Timeline



Sep 22, 2010:

9:06 PM Ticket #357 (Feature suggestion: function + binding to insert Coq closing tactics) created by Erik Martin-Dorel
I have noticed that Coq closing tactics are defined in …
8:34 PM Ticket #356 (Coq identifiers are unexpectedly colorized) created by Erik Martin-Dorel
I have just done a cvs update, and the Coq font lock seems to be …
4:11 PM Ticket #140 (PG takes a long time printing module types in Coq) closed by courtieu
fixed: This should be fixed now in cvs. Please let me know if there is still …
1:39 AM Ticket #352 (Unexpected shift in toolbar buttons) closed by David Aspinall
fixed: Confirmed, thanks for the recipe to reproduce this. Now fixed. It …
1:06 AM Ticket #355 (Autosend should be re-engaged after C-c C-n) created by David Aspinall
In case autosending is interrupted but the user hits C-c C-n, …

Sep 21, 2010:

6:09 PM Ticket #140 (PG takes a long time printing module types in Coq) reopened by Evgeny Makarov
I am sorry I did not respond to your requests for more information. I …

Sep 17, 2010:

11:30 AM Ticket #352 (Unexpected shift in toolbar buttons) reopened by Erik Martin-Dorel
The problem is actually reproducible when I use …

Sep 16, 2010:

3:29 PM Ticket #352 (Unexpected shift in toolbar buttons) closed by David Aspinall
needmoreinfo

Sep 14, 2010:

1:30 PM Ticket #354 (synchronisation lost with "process rest" and "undo") created by nils
this error is not really reproducible, but nevertheless occurs quite …
11:03 AM Ticket #353 ("undo last proof command" does not work at the end of theory) created by nils
there are only ML commands in this theory, and when it is processed …

Sep 12, 2010:

6:05 PM Ticket #352 (Unexpected shift in toolbar buttons) created by Erik Martin-Dorel
In the current ProofGeneral toolbar, the tooltip and underlying …

Sep 8, 2010:

6:18 PM Ticket #351 (Show/hide of proofs in Coq can hide too much) created by David Aspinall
As on the subject line. Test case: example.v, click on Hide for the …
1:53 PM Ticket #350 (Report Emacs bug (was: Unicode tokens "Reveal Control/Symbol Tokens" ...) created by David Aspinall
Test case: process a buffer, hide some proofs/comments containing …

Sep 3, 2010:

8:41 PM Ticket #349 (proof-process-buffer in a single shot (Mac OS X)) closed by David Aspinall
invalid: A feature! See Quick Options -> Fast Process Buffer. And a result of …
5:14 PM Ticket #349 (proof-process-buffer in a single shot (Mac OS X)) created by Makarius
This is Mac OS X with the no-nonsense version of GNU Emacs 23. Here …

Sep 1, 2010:

2:35 PM Ticket #346 (Coq multiple keywords are wrongly colorized) closed by courtieu
fixed: This is fixed in trunk now. Thanks a lot for the report.

Aug 30, 2010:

11:44 PM Ticket #348 (Need to update in coq-syntax.el the keywords containing the word Local) closed by David Aspinall
fixed: Fixed, many thanks. I also tweaked the abbrevs to match, hopefully …
11:38 PM Ticket #347 (Slight change in proof-store-buffer-win to enable undo in the Notepad) closed by David Aspinall
fixed: Done. Thanks for proposal.
7:21 PM Ticket #348 (Need to update in coq-syntax.el the keywords containing the word Local) created by Erik Martin-Dorel
The Coq keywords that contain the word Local should be updated in …
7:09 PM Ticket #347 (Slight change in proof-store-buffer-win to enable undo in the Notepad) created by Erik Martin-Dorel
The functions proof-store-goals-win and …
1:41 AM Ticket #346 (Coq multiple keywords are wrongly colorized) created by Erik Martin-Dorel
I have just noticed a bug in current font lock behavior: When a Coq …

Aug 29, 2010:

1:27 PM Ticket #345 (Semi-colons (';') cause outer syntax error: one command expected) created by Lucas Dixon
Using semi-colons used to be a handy way to control Proof General's …

Aug 28, 2010:

12:02 AM Ticket #344 (proof-retract-buffer incomplete) closed by David Aspinall
fixed: Thanks. A bug with nested spans and the find-forget loop. This was …

Aug 27, 2010:

8:52 PM Ticket #344 (proof-retract-buffer incomplete) created by Makarius
proof-retract-buffer fails to retract to the start of the …
1:00 AM Ticket #343 (Missing test in proof-store-buffer-win) closed by David Aspinall
fixed: Thanks for the report. Considering this further: I hadn't noticed …
12:01 AM Ticket #312 (Unicode tokens: add support for PhoX) closed by David Aspinall
wontfix: Not likely worthwhile, PhoX seems unlikely to be maintained.

Aug 26, 2010:

11:13 PM Ticket #343 (Missing test in proof-store-buffer-win) created by Erik Martin-Dorel
If I run proof-store-goals-win or proof-store-response-win

Aug 25, 2010:

9:26 AM Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") closed by David Aspinall
invalid: Aha. I had worried about this, many thanks for pointing out. Have …
1:05 AM Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") reopened by Erik Martin-Dorel
Hello, I reopen this ticket since I have just noticed that this …

Aug 24, 2010:

8:54 PM Ticket #335 (Script management: old-style undo broken in Isar) closed by David Aspinall
worksforme: Can't duplicate now, likely to do with changing undo mechanism during …
2:34 PM Ticket #287 (Script management flaws) closed by David Aspinall
fixed: Fixed a bug in Coq synchronization: proof-shell-restart was not …
2:03 PM Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") closed by David Aspinall
fixed: Fixed: proof-script-command-end-regexp now allows any …
12:51 PM Ticket #342 (Distracting error (actually raised by coq-command-at-point)) closed by David Aspinall
fixed: coq-command-at-point patched as suggested. Many thanks!
11:05 AM Ticket #342 (Distracting error (actually raised by coq-command-at-point)) created by Erik Martin-Dorel
The Coq/ProofGeneral/Emacs? interactive functions coq-insert-command, …

Aug 23, 2010:

6:48 PM Ticket #193 (Fix output of texi2html) closed by David Aspinall
fixed: Info entries and missing image fixed. Links seem OK. Too many …

Aug 22, 2010:

10:53 PM Ticket #340 (Key binding syntax in proof-splash.el) closed by David Aspinall
fixed: Ouch! Thanks for the fix, well spotted.
10:30 PM Ticket #341 (Suggestion to recover the default C-h suffix for Emacs keys help) closed by David Aspinall
fixed: Erik: many thanks for the excellent suggestion (and reminder of that …

Aug 21, 2010:

5:47 PM Ticket #341 (Suggestion to recover the default C-h suffix for Emacs keys help) created by Erik Martin-Dorel
The commands [C-c C-h] and [C-c C-a C-h] are currently assigned to the …

Aug 20, 2010:

6:21 PM Ticket #340 (Key binding syntax in proof-splash.el) created by Erik Martin-Dorel
When I do [C-h m] in the ProofGeneral splash screen, I see the …
12:31 AM Ticket #294 (Make pg-protected-undo allow in undo in comments of locked region) closed by David Aspinall
fixed: Fixed, thanks to patch of Erik Martin-Dore
12:07 AM Ticket #339 (Infinite loop on module print with coq-8.3) closed by David Aspinall
needmoreinfo: Strange! Thanks for the report and small example. Unfortunately …

Aug 19, 2010:

2:04 PM Ticket #339 (Infinite loop on module print with coq-8.3) created by Paolo Herms
When I try to process the following with coq 8.3 beta, emacs freezes …
10:39 AM Ticket #338 (Report Emacs bug: subscript and superscripts don't work with native ...) created by David Aspinall
See discussion in #280. This is not a fault of Proof General but of …

Aug 18, 2010:

4:20 PM MacBook created by David Aspinall
3:06 PM Ticket #326 (Strange warnings on Emacs for Mac OS X) closed by David Aspinall
invalid: Seems likely to be an Emacs issue: …
8:42 AM Ticket #337 (C-c C-a h is undefined) closed by Generic Isabelle user
duplicate: Duplicate of #334
1:41 AM Ticket #337 (C-c C-a h is undefined) created by igloo
When I use proof general with Isabelle, the "Isabelle/Show? me …

Aug 17, 2010:

7:55 PM Ticket #336 (Toolbar images on Mac Emacsen are super-ugly) created by David Aspinall
White background! Also seem to be magnified.
7:52 PM Ticket #335 (Script management: old-style undo broken in Isar) created by David Aspinall
Script management loses sync when Isabelle -> Settings -> Use Linear …
6:23 PM Ticket #332 (Minibuffer display of first line of urgent messages lost?) closed by David Aspinall
invalid: It's now an option to reduce noise. Enable with Quick Options -> …
6:19 PM Ticket #333 (Restart tool button points to manual) closed by David Aspinall
worksforme: Strange. Can't repeat this in Ubuntu 10.04, 23.1.1. What is precise …
6:17 PM Ticket #334 (Broken Keybindings for Show Me -> ... and others) closed by David Aspinall
fixed: Fixed, many thanks for reporting. I think the bindings used an XEmacs …
2:59 PM Ticket #334 (Broken Keybindings for Show Me -> ... and others) created by Generic Isabelle user
Using Proof General 4.0pre100709, 4.0pre100815 or 3.7.11 and Gnu Emacs …

Aug 16, 2010:

8:03 PM Ticket #333 (Restart tool button points to manual) created by Makarius
This is Xubuntu 10.04 LTS, GNU Emacs 23.1.1. In the toolbar, the …
8:01 PM Ticket #332 (Minibuffer display of first line of urgent messages lost?) created by Makarius
This is Xubuntu 10.04 LTS, GNU Emacs 23.1.1. It seams that the …
12:12 AM Ticket #330 (Error raised by proof-issue-goal and proof-issue-save) closed by David Aspinall
fixed: Fixed, many thanks for making the report. (please note: this Trac …
12:00 AM Ticket #331 (Coq config for proof-goal-command and proof-save-command) closed by David Aspinall
fixed: Done, thanks.

Aug 14, 2010:

10:58 AM Ticket #331 (Coq config for proof-goal-command and proof-save-command) created by Erik Martin-Dorel
The convenient functions proof-issue-goal and proof-issue-save

Aug 13, 2010:

11:51 PM Ticket #330 (Error raised by proof-issue-goal and proof-issue-save) created by Erik Martin-Dorel
When I run the function proof-issue-goal or proof-issue-save (e.g. …

Aug 11, 2010:

9:06 PM Ticket #288 (Splash screen misbehaves) closed by David Aspinall
fixed: Fixed by reverting to a version of the original code. Experimenting …
12:24 AM Ticket #329 (Unwanted kill-buffer at startup) closed by David Aspinall
duplicate: Thanks for making the report, it is appreciated. This is a symptom of …

Aug 7, 2010:

12:02 PM Ticket #329 (Unwanted kill-buffer at startup) created by Erik Martin-Dorel
Hi, I have noticed that when I run ProofGeneral, i.e. at the time I …

Aug 6, 2010:

4:43 PM Ticket #324 (Script management very slow on some platforms) reopened by Makarius
4:26 PM Ticket #328 (Strange resizing of main buffer after minibuffer dialog corres) closed by Makarius
invalid: I have tried again on a completely different installation of Ubuntu …

Aug 4, 2010:

6:39 PM Ticket #328 (Strange resizing of main buffer after minibuffer dialog corres) reopened by Makarius
Er, well this is Emacs 23.1.1, not Emacs 22. This is the standard GNU …
1:25 AM Ticket #328 (Strange resizing of main buffer after minibuffer dialog corres) closed by David Aspinall
invalid: I tried briefly to reproduce this but couldn't. Would likely need …
1:15 AM Ticket #327 (Elisp stack overflow when retracting many files at once) closed by David Aspinall
fixed: Hmm, thought I had fixed this already in #274. but forgot Emacs Lisp …
1:01 AM Ticket #324 (Script management very slow on some platforms) closed by David Aspinall
needmoreinfo: There is now a mechanism for testing and profiling triggered by "make …

Aug 3, 2010:

8:32 PM Ticket #328 (Strange resizing of main buffer after minibuffer dialog corres) created by Makarius
This is GNU Emacs 23.1.1 on Xubuntu 9.10. Visiting (or revisiting) a …
5:28 PM Ticket #327 (Elisp stack overflow when retracting many files at once) created by Makarius
This is Emacs 23.2.1 on Mac OS X (no-nonsense version), or GNU Emacs …
4:53 PM Ticket #326 (Strange warnings on Emacs for Mac OS X) created by Makarius
This is the "no-nonsense" version from http://emacsformacosx.com -- …

Jul 26, 2010:

10:02 AM Ticket #325 (Splash buffer occupies half the frame) closed by David Aspinall
duplicate: Thanks for the report. I agree with what you say! This will be fixed …

Jul 24, 2010:

1:06 PM Ticket #325 (Splash buffer occupies half the frame) created by Evgeny Makarov
Hello, In the past, when PG was started, Emacs showed the splash …

Jul 11, 2010:

8:12 PM Ticket #324 (Script management very slow on some platforms) reopened by Makarius
IIRC, the jEdit timing was on the same machine as the other "Mac OS X" …

Jul 9, 2010:

12:22 AM Ticket #324 (Script management very slow on some platforms) closed by David Aspinall
needmoreinfo: Would be useful to know more, e.g., have some profiling information …
12:16 AM Ticket #323 (Strange errors of make compile concerning save-excursion/set-buffer) closed by David Aspinall
fixed: Thanks for the log. I forgot to commit the remainder of the fixes. …

Jul 5, 2010:

5:19 PM Ticket #324 (Script management very slow on some platforms) created by Makarius
Script management seems to be quite slow on some platforms / Emacs …
10:32 AM Ticket #323 (Strange errors of make compile concerning save-excursion/set-buffer) reopened by Makarius

Jul 1, 2010:

11:21 PM Ticket #323 (Strange errors of make compile concerning save-excursion/set-buffer) closed by David Aspinall
fixed: OK, struggled a while with library mess and built latest Emacs and …
10:49 PM Ticket #314 (Duplication of some special messages) closed by David Aspinall
fixed: Fix confirmed by a second person, so closing now.
4:39 PM Ticket #323 (Strange errors of make compile concerning save-excursion/set-buffer) created by Makarius
This is GNU Emacs 23.2.1 on Mac OS. Byte-compilation via {{{make …

Jun 28, 2010:

8:44 AM Ticket #290 (Undo and delete for token input don't behave as expected) closed by David Aspinall
fixed: Fixed, for now. Added some key bindings to delete tokens and undo …

Jun 27, 2010:

1:57 PM Ticket #321 (Retract buffer broken) closed by David Aspinall
needmoreinfo: Can't reproduce this without a concrete example. I am seeing sync …
Note: See TracTimeline for information about the timeline view.