Timeline


and .

11/16/09:

17:48 Ticket #299 (Out of sync with Isabelle) closed by da
needmoreinfo
17:48 Ticket #305 (High overhead) closed by da
needmoreinfo: This generally shouldn't be the case, but it depends on the circumstances. …

11/12/09:

13:43 Ticket #305 (High overhead) created by NorbertSchirmer
When processing larger portions (thousands of lines) of a Isabelle theory …
10:35 Ticket #304 (Isabelle: trying to undo a step fails for me) closed by RafalKolanski
invalid: Actually, nevermind, turns out our version of Isabelle doesn't have …
10:24 Ticket #304 (Isabelle: trying to undo a step fails for me) created by RafalKolanski
I am uncertain if my version of Isabelle is to blame (i.e. not *exactly* …

11/11/09:

10:45 Ticket #303 (underlining on error sucks) created by krauss
While others may report more fundamental problems, here is another …

11/06/09:

23:38 Ticket #301 (Ubuntu 9.10: PG menus broken) closed by da
invalid: Confirmed, at least for Emacs 22. For goodness sake, how on earth did …
23:26 Ticket #302 (Coq mode requires hilit19.el which is not in Emacs 23) closed by da
invalid: Thanks for reporting but I'm sorry, I can't find the dependency that …
03:06 Ticket #302 (Coq mode requires hilit19.el which is not in Emacs 23) created by wolverian
On Ubuntu 9.10, the emacs23 package does not include hilit19.el, which the …

11/05/09:

14:26 Ticket #301 (Ubuntu 9.10: PG menus broken) created by makarius
On Ubuntu 9.10 with Emacs 22 or 23, the PG specific menus are broken …
14:22 Ticket #300 (Emacs 22: strange keyword categorization) created by makarius
This is Ubuntu 9.10 with GNU Emacs 22 (Gtk). Somehow the keyword …

10/21/09:

21:22 Ticket #292 (Goal buffer not updated on "undo" and "goto) reopened by makarius
In the old protocol with non-linear undo, it worked via the …

10/19/09:

09:41 Ticket #299 (Out of sync with Isabelle) created by NorbertSchirmer
When working within Isar proofs ProofGeneral and Isabelle get out of sync …

10/16/09:

17:49 Ticket #298 (Isabelle indentation) created by NorbertSchirmer
The automatic indentation for Isar proofs has some …
12:47 Ticket #297 (Finding of lisp relative to the "proofgeneral" script is broken) closed by da
fixed: Many thanks for the patch, have added in CVS now.
08:14 Ticket #297 (Finding of lisp relative to the "proofgeneral" script is broken) created by mattmccutchen
I'm glad to see that support for finding the lisp files relative to the …
06:32 Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") created by mattmccutchen
If I type the following complete garbage and press "C-c C-RET" at the end …

10/05/09:

18:55 Ticket #295 (Undo on edit in ML-sections) created by krauss
It appears that undo-on-edit does not work when editing within an ML {* …
13:20 Ticket #293 (Synchronisation losses with undo-on-edit) closed by da
fixed: Thanks for follow-up. Assuming you only lose key-presses in the case …

10/03/09:

18:36 Ticket #294 (Make pg-protected-undo allow in undo in comments of locked region) created by da
Editing is allowed in comments inside the locked region, but the protected …

10/02/09:

11:20 Ticket #293 (Synchronisation losses with undo-on-edit) created by krauss
The following behaviour makes the setting "PG -> Quick Options -> Read …

09/27/09:

00:58 Ticket #291 (3-Panel-mode: Strange buffer switch when loading a theory) closed by da
fixed: Fixed in CVS. Thanks for the report. The code tried to do something …

09/26/09:

14:02 Ticket #292 (Goal buffer not updated on "undo" and "goto) closed by da
fixed: Thanks for the report. Assume you are using Isabelle with the new …

09/25/09:

15:37 Ticket #292 (Goal buffer not updated on "undo" and "goto) created by krauss
in 4.0pre090921 under GNU Emacs 23.1.1 at these commands, the goal …

09/23/09:

15:20 Ticket #291 (3-Panel-mode: Strange buffer switch when loading a theory) created by krauss
Steps to reproduce: 1. Proof General -> Quick Options -> Display -> …

09/21/09:

15:03 Ticket #281 (Odd unicode abbreviations, notably |>) closed by da
fixed: Moved to #290.
15:03 Ticket #290 (Improve and document undo behaviour for token input) created by da
Ordinary undo with token input does not behave as the user might expect …
15:00 Ticket #227 (Recover active scripting modeline indicator) closed by da
fixed: Actually, this seems fine really. Now it is pink.
14:57 Ticket #285 (byte compilation) closed by da
fixed: Byte compilation should be working now. The distribution now includes …

09/20/09:

21:22 Ticket #289 (Drawback of command wrapping in PG+Isar) closed by da
fixed: Fixed in proof-script.el 10.44, which makes …
21:16 Ticket #289 (Drawback of command wrapping in PG+Isar) reopened by da

09/17/09:

08:48 Ticket #289 (Drawback of command wrapping in PG+Isar) closed by da
invalid: [Followup from Makarius]: I have already noticed that the …

09/16/09:

16:56 Ticket #289 (Drawback of command wrapping in PG+Isar) created by da
[message from Lucas Dixon] (PG: 4.0pre090916) I used to sprinkle …

09/14/09:

09:22 Ticket #288 (Splash screen misbehaves) created by da
This is just a note that the splash screen (simplified to use built in …
09:16 Ticket #170 (Improve outline syntax for Isar) closed by da
fixed: Level support now added for GNU Emacs, using `outline-heading-list'. …

09/11/09:

01:31 Ticket #287 (Script management flaws) created by da
Some of the script management code has been generalised and (for Isabelle) …
01:28 Ticket #278 (Resolve pointer-movement issues during script management) closed by da
fixed: This is satisfactory for now. There is still a small glitch where the …
01:23 Ticket #284 (proof-process-buffer very slow) closed by da
fixed: The main reason turned out to be an experiment with …

09/09/09:

19:39 Ticket #258 (Copying from response buffer also copies colour control chars) closed by da
fixed: This has been fixed in CVS now (since about May this year, actually).
12:51 Ticket #286 (PG startup crash) closed by da
fixed: Thanks. I have added a compatibility patch for this but notice from …

09/07/09:

23:18 Ticket #286 (PG startup crash) created by makarius
GNU Emacs 22.1.1, Ubuntu 8.04 LTS. PG startup crashes: {{{File mode …

09/04/09:

17:00 Ticket #285 (byte compilation) created by makarius
GNU Emacs 23.1.1 on Mac OS, Proof General 4.0pre090902 (or CVS …
12:22 Ticket #191 (Code cleanup: remove proof-no-command) closed by da
fixed: Have fixed now in script code refactoring.
12:21 Ticket #191 (Code cleanup: remove proof-no-command) reopened by da
12:20 WikiStart edited by da
(diff)
12:19 WikiStart edited by da
(diff)
12:17 WikiStart edited by da
(diff)

09/03/09:

10:07 Ticket #282 (Emacs 23.1.1 on Mac OS: no toolbar) closed by da
invalid: Not a PG issue, seems to be an option in the Mac OS X port. You can …
09:54 Ticket #283 (assert command etc.: strange movement of point) closed by da
duplicate: Known, but thanks. See #278

09/02/09:

15:53 Ticket #284 (proof-process-buffer very slow) created by makarius
GMU Emacs 23.1.1, Mac OS. Asserting a whole buffer via …
15:37 Ticket #283 (assert command etc.: strange movement of point) created by makarius
GNU Emacs 23.1.1, Mac OS. The point movement after asserting commands …
13:16 Ticket #282 (Emacs 23.1.1 on Mac OS: no toolbar) created by makarius
The PG tool seems to be missing on this platform.
11:32 Ticket #281 (Odd unicode abbreviations, notably |>) created by makarius
In isar-symbol-shortcuts there are some odd abbreviations, notably …

08/31/09:

21:42 Ticket #280 (Unicode Tokens: cleanups) created by da
Final 4.0 cleanups: * choice of default fonts: see if can get …
16:57 Ticket #274 (Max lisp nesting exceeded on large error outputs) closed by da
fixed: I've fixed, `isar-remove-line' was not recursing indefinitely, but was …
14:24 Ticket #211 (Coq : deactivation of the 'Holes' functionality) closed by courtieu
fixed: The patch seems ok to me. holes completion in abbreviations is now …
09:58 Ticket #279 (Proof visibility controls broken) created by da
With additional spans in the buffer the individual visibility control for …
09:56 Ticket #277 (span start vs. command start) closed by da
fixed: Thanks for report. Fixed now but see #278.
09:56 Ticket #278 (Resolve pointer-movement issues during script management) created by da
Pointer movement control cleanup is in progress, at the moment there are …

08/28/09:

21:42 Ticket #277 (span start vs. command start) created by makarius
GNU Emacs 22.1.1, Ubuntu 8.04 LTS, Isabelle2009. The span passed to …
12:13 Ticket #276 (Unicode tokens: resolve font-lock issues, optimise) created by da
Unicode tokens interacts closely with font lock but there was a problem …
Note: See TracTimeline for information about the timeline view.