Timeline



Feb 17, 2008:

12:44 PM Ticket #204 (undo stops undoing in large proofs) closed by David Aspinall
fixed: Thanks for raising this. I've added an item to the FAQ, and also …
12:35 PM Ticket #201 (X-Symbol only half enabled (Emacs: yes, prover: no)) closed by David Aspinall
fixed: Fixed. Caused by clash with Unicode Tokens (which promptly turned off …
11:57 AM Ticket #202 (Prover chokes on Unicode Tokens (Carbon Emacs)) closed by David Aspinall
fixed: Fixed: left over experimental code removed. This mode is being …

Feb 15, 2008:

12:13 AM Ticket #204 (undo stops undoing in large proofs) created by mccreight
In large Coq proofs (with more than 100 lines), undo stops working. …

Feb 13, 2008:

3:40 PM Ticket #203 (Carbon Emacs: no colouring of variables in Isabelle output) created by Makarius
E.g. printing term "x" merely shows a black "x", not a blue one as …
3:38 PM Ticket #202 (Prover chokes on Unicode Tokens (Carbon Emacs)) created by Makarius
After a recent change in the unicode token mode, the prover chokes on …
3:35 PM Ticket #201 (X-Symbol only half enabled (Emacs: yes, prover: no)) created by Makarius
Linux (SuSE or Ubuntu) and xemacs-21.4.x Running the …

Feb 8, 2008:

11:29 AM Ticket #200 (Sledgehammer output broken) created by David Aspinall
Output appears in *isabelle* buffer but not response buffer. …

Feb 7, 2008:

9:42 AM Ticket #199 (Allow use of Isabelle.command to wrap commands singly) created by David Aspinall
Isabelle.command allows additional "properties" to be attached to …

Feb 6, 2008:

11:52 PM Ticket #197 (Non-persistance of Unicode Tokens / Math Menu (Carbon Emacs 1.6.0)) closed by David Aspinall
fixed: Thanks for the report. Not just Carbon! A generic problem, …
3:52 PM Ticket #198 (Prover executable not found when running without interface script) created by Makarius
Using Carbon Emacs 1.6.0 without the isar/interface script, but …
3:39 PM Ticket #197 (Non-persistance of Unicode Tokens / Math Menu (Carbon Emacs 1.6.0)) created by Makarius
Using native Carbon Emacs 1.6.0 on Mac OS 10.4.x the Unicode Tokens …

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). …
Note: See TracTimeline for information about the timeline view.