Timeline
Sep 29, 2010:
- 10:33 AM Ticket #356 (Coq identifiers are unexpectedly colorized) reopened by
- Thanks for the fix. But I reopen the ticket since it seems to me …
Sep 28, 2010:
- 8:29 PM Ticket #360 (link to proof general is broken and lacks helpful message) created by
- The link to Proof General 4.0 on …
- 5:34 PM Ticket #356 (Coq identifiers are unexpectedly colorized) closed by
- fixed: This should be fixed in cvs now. Thanks a lot for reporting.
Sep 27, 2010:
- 1:53 AM Ticket #359 (Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & ...) created by
- I suggest to fix 3 key bindings issues in coq/coq.el: The correct …
- 1:24 AM Ticket #358 (link to proof general is broken) closed by
- invalid: Not a bug, 4.0 not yet released. Sorry for confusion.
Sep 25, 2010:
- 7:47 PM Ticket #358 (link to proof general is broken) created by
- The link to Proof General 4.0 on …
Sep 22, 2010:
- 9:06 PM Ticket #357 (Feature suggestion: function + binding to insert Coq closing tactics) created by
- I have noticed that Coq closing tactics are defined in …
- 8:34 PM Ticket #356 (Coq identifiers are unexpectedly colorized) created by
- 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
- 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
- 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
- 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
- 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
- The problem is actually reproducible when I use …
Sep 16, 2010:
Sep 14, 2010:
- 1:30 PM Ticket #354 (synchronisation lost with "process rest" and "undo") created by
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- The functions
proof-store-goals-win
and … - 1:41 AM Ticket #346 (Coq multiple keywords are wrongly colorized) created by
- 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
- 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
- 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
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
- 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
- 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
- If I run
proof-store-goals-win
orproof-store-response-win
…
Aug 25, 2010:
- 9:26 AM Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") closed by
- 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
- 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
- worksforme: Can't duplicate now, likely to do with changing undo mechanism during …
- 2:34 PM Ticket #287 (Script management flaws) closed by
- 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
- 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
- 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
- The Coq/ProofGeneral/Emacs? interactive functions
coq-insert-command
, …
Aug 23, 2010:
- 6:48 PM Ticket #193 (Fix output of texi2html) closed by
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- See discussion in #280. This is not a fault of Proof General but of …
Aug 18, 2010:
- 4:20 PM MacBook created by
- 3:06 PM Ticket #326 (Strange warnings on Emacs for Mac OS X) closed by
- invalid: Seems likely to be an Emacs issue: …
- 8:42 AM Ticket #337 (C-c C-a h is undefined) closed by
- duplicate: Duplicate of #334
- 1:41 AM Ticket #337 (C-c C-a h is undefined) created by
- 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
- White background! Also seem to be magnified.
- 7:52 PM Ticket #335 (Script management: old-style undo broken in Isar) created by
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- fixed: Done, thanks.
Aug 14, 2010:
- 10:58 AM Ticket #331 (Coq config for proof-goal-command and proof-save-command) created by
- The convenient functions
proof-issue-goal
andproof-issue-save
…
Aug 13, 2010:
- 11:51 PM Ticket #330 (Error raised by proof-issue-goal and proof-issue-save) created by
- When I run the function
proof-issue-goal
orproof-issue-save
(e.g. …
Aug 11, 2010:
- 9:06 PM Ticket #288 (Splash screen misbehaves) closed by
- fixed: Fixed by reverting to a version of the original code. Experimenting …
- 12:24 AM Ticket #329 (Unwanted kill-buffer at startup) closed by
- 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
- 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
- 4:26 PM Ticket #328 (Strange resizing of main buffer after minibuffer dialog corres) closed by
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
Jul 1, 2010:
- 11:21 PM Ticket #323 (Strange errors of make compile concerning save-excursion/set-buffer) closed by
- 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
- 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
- This is GNU Emacs 23.2.1 on Mac OS. Byte-compilation via {{{make …
Note: See TracTimeline
for information about the timeline view.