Timeline



Feb 3, 2008:

2:28 PM Ticket #196 (Fix X-Symbol for Emacs 23) created by David Aspinall
X-Symbol in Emacs 23 is disabled in PG 3.7 because of breakage due to …

Feb 1, 2008:

12:17 AM WikiStart edited by David Aspinall
(diff)
12:16 AM WikiStart edited by David Aspinall
(diff)
12:09 AM Ticket #195 (Replace crufty PHP code for interpreting outline mode with some Javascript) created by David Aspinall
There is some crufty PHP code for displaying Emacs outline files, e.g. …
12:07 AM Ticket #194 (Fix links on web pages and odd mime types for linked files under releases) created by David Aspinall
The home page links (click on the general) are no longer working. …
12:01 AM Ticket #193 (Fix output of texi2html) created by David Aspinall
Several glitches are now appearing in the user manuals, including …

Jan 31, 2008:

11:50 PM Milestone PG-Emacs-3.7 completed
Next PG release aimed to coincide with Isabelle2007. …
10:24 PM Ticket #192 (Improve out-of-the-box behaviour for some common configurations) created by David Aspinall
Several places, e.g.: * Compatibility with the standard Coq Windows …

Jan 30, 2008:

1:59 PM Ticket #118 (Complete X-Symbol unicode patch and add symbol configuration for Isabelle) closed by David Aspinall
wontfix: I now view this as a dead-end. The X-Symbol code is too crufty and …

Jan 29, 2008:

9:18 PM Ticket #184 (lib/maths-menu.el doesn't compile on XEmacs 21.4) closed by David Aspinall
fixed: This file doesn't work in XEmacs 21.4, and getting it to compile there …
9:17 PM Ticket #178 (Emacs occasionally hangs when doing isearch-forward.) closed by David Aspinall
worksforme
8:31 PM Ticket #189 (Undo does not work for diagnostic commands in proofs) closed by David Aspinall
fixed: Fixed. Thanks for reporting this. It was caused by a half-complete …
8:29 PM Ticket #191 (Code cleanup: remove proof-no-command) created by David Aspinall
We could replace proof-no-command simply by nil.
7:55 PM Ticket #186 (Failed initialization of *trace* buffer (xemacs-21.4.x)) closed by David Aspinall
duplicate: Duplicate of #183
7:55 PM Ticket #183 (ProofGeneral crashes when displaying tracing messages) closed by David Aspinall
fixed: Thanks for spotting this! Fixed now, but see #190.
7:53 PM Ticket #190 (Improve proof shell initialisation order) created by David Aspinall
Init order in proof-shell-start is tricky, because the shell mode sets …
9:39 AM Ticket #189 (Undo does not work for diagnostic commands in proofs) created by Stefan Berghofer
When trying to undo a diagnostic command (such as thm) occurring …
5:20 AM Ticket #188 (Option to treat comments as individual statements.) created by RafalKolanski
The commands of type (* comment *) and -- "comment" are absorbed as …
5:15 AM Ticket #187 (If sent command fails, don't move the cursor.) created by RafalKolanski
Typical work flow is: change something, send using c-c c-return. If …

Jan 28, 2008:

12:55 PM Ticket #185 (Failed initialization of *trace* buffer (xemacs-21.4.x)) closed by Makarius
duplicate
12:53 PM Ticket #186 (Failed initialization of *trace* buffer (xemacs-21.4.x)) created by Makarius
Using xemacs-21.4.x (on Mac OS or Linux), the initial *trace* buffer …
12:53 PM Ticket #185 (Failed initialization of *trace* buffer (xemacs-21.4.x)) created by Makarius
Using xemacs-21.4.x (on Mac OS or Linux), the initial *trace* buffer …
11:45 AM Ticket #184 (lib/maths-menu.el doesn't compile on XEmacs 21.4) created by courtieu
[…] I am using debian unstable xemacs version: 21.4 (patch 21)…
11:16 AM Ticket #183 (ProofGeneral crashes when displaying tracing messages) created by Stefan Berghofer
ProofGeneral crashes while trying to display tracing messages produced …

Jan 27, 2008:

11:44 AM Ticket #181 (Strange font-lock warning/error in GNU Emacs 21.4.1 (Ubuntu 7.10)) closed by David Aspinall
fixed: Fixed. Same issue as #182.
11:44 AM Ticket #182 (Problem with sub/superscript in GNU Emacs 21.4.1 (Ubuntu 7.10)) closed by David Aspinall
fixed: Fixed in CVS. Caused by improvement in sub/super handling enabled for …

Jan 26, 2008:

4:57 PM Ticket #182 (Problem with sub/superscript in GNU Emacs 21.4.1 (Ubuntu 7.10)) created by Makarius
In GNU Emacs 21.4.1 (Ubuntu 7.10) sub/superscript control sequences …
4:31 PM Ticket #181 (Strange font-lock warning/error in GNU Emacs 21.4.1 (Ubuntu 7.10)) created by Makarius
Starting Proof General with GNU Emacs 21.4.1 (Ubuntu 7.10) produces …

Jan 25, 2008:

11:56 PM Ticket #180 (Sub/superscript sometimes not rendered properly.) closed by David Aspinall
fixed: Fixed. It happened when the process died, caused by a bug in …
10:18 PM Ticket #180 (Sub/superscript sometimes not rendered properly.) created by Makarius
Using GNU emacs 22.1.1 on Ubuntu 7.10, \<^sub> and {{{ \<sup> …
10:12 PM Ticket #179 (Losing sync with interrupt) created by Makarius
Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor easily looses sync …
10:10 PM Ticket #178 (Emacs occasionally hangs when doing isearch-forward.) created by Makarius
Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor occasionally hangs …
6:53 PM Ticket #177 (Complete Unicode Token coding system and input method) created by David Aspinall
This is an experimental partial replacement for X-Symbol. Ultimately …
6:02 PM Ticket #176 (Allow isabelle-chosen-logic to be set by variable comment in thy file) created by David Aspinall
At the moment a comment like […] doesn't work as desired because …
4:15 PM Ticket #175 (ProofGeneral accidentally resets itself while scrolling) closed by David Aspinall
fixed: Fixed, I hope: backward compatibility patch for XEmacs 21.4 added to …
4:15 PM Ticket #174 (Unable to exit prover) closed by David Aspinall
fixed: Fixed, I hope: backward compatibility patch for XEmacs 21.4 added to …
3:35 PM Ticket #173 (coq indenting mode gets confused by *) in proofs) closed by David Aspinall
fixed: Thanks for the report. I've added a patch which seems to fix this …
2:51 PM Ticket #175 (ProofGeneral accidentally resets itself while scrolling) created by Stefan Berghofer
When using ProofGeneral with XEmacs 21.4 and the CVS version of …
2:33 PM Ticket #174 (Unable to exit prover) created by Stefan Berghofer
When using ProofGeneral with XEmacs 21.4 and the CVS version of …
1:05 AM Ticket #173 (coq indenting mode gets confused by *) in proofs) created by Jacob Matthews
Using the latest CVS version of pg-emacs (as of Thu Jan 24 16:48:42 …

Jan 24, 2008:

11:23 PM Ticket #172 (Problem with indentation in Coq mode) closed by Proof General Developer
fixed: Now fixed. Many thanks for the report! Code in coq-indent.el used …
7:26 PM Ticket #171 (Documentation fix for Isabelle keybindings) closed by Proof General Developer
fixed: Applied now to CVS. Many thanks for taking the trouble to upload …

Jan 19, 2008:

3:53 PM Ticket #172 (Problem with indentation in Coq mode) created by Alexandre Pilkiewicz
While editing a Coq script proof file, the indentation does not work. …

Jan 18, 2008:

5:20 PM Ticket #171 (Documentation fix for Isabelle keybindings) created by Mark A. Hillebrand
Hi, the attached patch fixes the documentation of the special …

Jan 15, 2008:

11:40 PM Ticket #119 (Fix compilation problems, missing files) closed by David Aspinall
fixed: Compilation now fixed, following some heavy re-organisation of files …
11:37 PM Ticket #161 (The font-lock setup misbehaves when started via menu) closed by David Aspinall
fixed: Fixed in proof-x-symbol.el 8.10 (proof-x-symbol-decode-region). …

Dec 14, 2007:

4:29 PM Ticket #119 (Fix compilation problems, missing files) reopened by David Aspinall
Unfortunately there are still some nasty compile issues around macro …
3:50 PM Ticket #120 (Fix docstring magic to interpret blank lines as whitespace inside ...) closed by David Aspinall
fixed
12:58 PM Ticket #170 (Improve outline syntax for Isar) created by David Aspinall
Outline syntax only contains theory headings at the moment. Perhaps …
12:56 PM Ticket #119 (Fix compilation problems, missing files) closed by David Aspinall
fixed: da: I have fixed the compile problems for Coq now, with some …
12:44 AM Ticket #112 (Filter out control characters in shell buffer or copy from shell buffer) closed by Proof General Developer
fixed: Now fixed (in proof-shell.el) by cleaning up the output after it's …

Dec 13, 2007:

11:24 PM Ticket #169 (Complete buffer history enhancement) created by Proof General Developer
The buffer history addition is not quite ready, so pulled from 3.7. …
9:51 PM Ticket #88 (Buffer invisibility spec bug with Emacs 22) closed by David Aspinall
worksforme: Problems not seen with released and supported Emacs version 22.1.1, so …
8:37 PM Ticket #129 (X-Symbol in GNU Emacs: fix support for hiding tokens \<^loc>, \<bsub>, etc) closed by David Aspinall
fixed: Now works well with Emacs 22.1.1: font lock properties are now able to …
8:29 PM Ticket #117 (Add resized toolbar icons) closed by David Aspinall
fixed

Dec 12, 2007:

7:44 PM WikiStart edited by David Aspinall
(diff)

Dec 10, 2007:

10:52 AM Ticket #168 (Reorganise TODO files in distribution) created by David Aspinall
Most of the TODO/todo files are obsolete. Some may have tasks worth …

Dec 9, 2007:

5:34 PM Ticket #165 (Cygwin: font-lock crashes on XEmacs 21.4.20) closed by David Aspinall
wontfix: Thanks for the report. Unfortunately I'm not able to test on Cygwin …
5:27 PM Ticket #164 (Error with GNU Emacs 21.4.1/C-c C-BS) closed by David Aspinall
wontfix: Thanks for this bug report. Unfortunately this version of Emacs has …
3:31 PM Ticket #152 (Faults with main regexps in XEmacs 21.5(b28) for Coq) closed by David Aspinall
fixed: Regexps were failing because s- was not matching newlines. It …

Dec 8, 2007:

7:28 PM Ticket #167 (GNU Emacs 22.1.1 allows only one undo in a row from the toolbar while ...) closed by David Aspinall
invalid: Thanks for the report, Ralph. Unfortunately I can't reproduce this …
7:13 PM Ticket #163 (Problems with x-symbol in XEmacs 21.5.28 (latin-iso8859-2 error)) closed by David Aspinall
fixed: This is a bug in x-symbol-mule.el for XEmacs 21.5.28 (present in …

Nov 29, 2007:

2:23 PM Ticket #167 (GNU Emacs 22.1.1 allows only one undo in a row from the toolbar while ...) created by An Isabelle Developer
I use Isabelle 2007 with PG 3.7pre071112 under GNU Emacs 22.1.1 …

Nov 28, 2007:

12:00 PM Ticket #166 (Out of sync on illegal escape character) created by Peter Lammich
PG-Emacs: 3.7pre071112 Isabelle: 2007 Here is a reproducible way to …

Nov 20, 2007:

4:49 PM Ticket #165 (Cygwin: font-lock crashes on XEmacs 21.4.20) created by An Isabelle Developer
Certain complex response from the prover (Isabelle2007) can make …

Nov 16, 2007:

3:26 PM Ticket #164 (Error with GNU Emacs 21.4.1/C-c C-BS) created by David Aspinall
I'm going through the "walkthrough example in Isabelle/Isar?" in …
1:04 PM Ticket #121 (Add download counter to web) closed by Graham Dutton
fixed: Implemented at http://proofgeneral.inf.ed.ac.uk/decant/ (stats page …

Nov 14, 2007:

5:48 PM WikiStart edited by David Aspinall
(diff)
5:35 PM ProofGeneral edited by David Aspinall
(diff)
5:34 PM ProofGeneral created by David Aspinall
5:33 PM Ticket #163 (Problems with x-symbol in XEmacs 21.5.28 (latin-iso8859-2 error)) created by Stefan Berghofer
I'm just trying to get ProofGeneral to work with XEmacs 21.5.28 and …
5:27 PM WikiStart edited by David Aspinall
(diff)
5:23 PM Ticket #162 (Compatibility ProofGeneral-3.7pre071025, Isabelle, XEmacs 21.5.28) closed by David Aspinall
invalid: Thanks for the report, appreciated. This should work. The backtrace …
1:25 PM Ticket #162 (Compatibility ProofGeneral-3.7pre071025, Isabelle, XEmacs 21.5.28) created by Mark A. Hillebrand
Isabelle fails to start up with PG 3.7 and XEmacs 21.5.28, not sure if …
10:09 AM Ticket #161 (The font-lock setup misbehaves when started via menu) created by Makarius
The font-lock setup does not handle \<^sub> and \<^sub> properly …

Nov 12, 2007:

6:56 PM Ticket #157 (undo sometimes incorrectly tries to undo a larger container than is ...) closed by David Aspinall
duplicate: Thanks for the notes. The broken behaviour isn't your fault; I …
6:15 PM Ticket #160 ("Abort" keyword not recognized in Coq) closed by David Aspinall
fixed: Fix added, many thanks for report.
6:08 PM WikiStart edited by David Aspinall
(diff)
12:35 AM Ticket #160 ("Abort" keyword not recognized in Coq) created by scsibug
Indentation is not closed properly after an "Abort." statement, …

Nov 7, 2007:

5:59 PM Ticket #159 (Goal centering) created by mccreight
Is it possible to have the centering behavior of the *goals* window be …
Note: See TracTimeline for information about the timeline view.