#450 |
Proof in proof tree
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#279 |
Proof visibility controls broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#458 |
ProofGeneral 4.2 byte-compilation fails with Emacs 24.2.90
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#175 |
ProofGeneral accidentally resets itself while scrolling
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#183 |
ProofGeneral crashes when displaying tracing messages
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#493 |
ProofGeneral stalls/loops on ...
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#471 |
ProofGeneral.jpg missing in ProofGeneral-4.3pre130510.tgz
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#202 |
Prover chokes on Unicode Tokens (Carbon Emacs)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#198 |
Prover executable not found when running without interface script
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#139 |
Prover not started when run from Product
|
Graham Dutton
|
defect
|
critical
|
|
1:pg-eclipse
|
#227 |
Recover active scripting modeline indicator
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#253 |
Refactor to allow more converter objects, investigate conversion mechanisms
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#220 |
Remove X-Symbol, XEmacs support and backward compatibility
|
David Aspinall
|
task
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#84 |
Remove double-quoted XML output from term display
|
David Aspinall
|
defect
|
blocker
|
|
4:prover-isabelle
|
#238 |
Remove goto thread
|
Graham Dutton
|
defect
|
major
|
|
1:pg-eclipse
|
#168 |
Reorganise TODO files in distribution
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#126 |
Repair symbol handling
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#24 |
Replace current undo management with document-based undo mechanism
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#350 |
Report Emacs bug (was: Unicode tokens "Reveal Control/Symbol Tokens" reveals hidden text in script buffer)
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#381 |
Report Emacs bug/issue: slow process filter behaviour on non-Linux platforms
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#405 |
Report Emacs bug: Quail input breaks delete-char behaviour
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#338 |
Report Emacs bug: subscript and superscripts don't work with native Mac OS Emacsen
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#317 |
Report emacs bug: overlapping visibility properties
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#318 |
Report emacs bug: segfault with use of display property/font-lock
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#278 |
Resolve pointer-movement issues during script management
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#333 |
Restart tool button points to manual
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#229 |
Restore mouse and button actions in goals buffers
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#228 |
Restore tracing slow mode if necessary
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#321 |
Retract buffer broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#443 |
Retracting, editing, then re-evaluating/proving sometimes results in definitions that do not match the contents of the file
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#287 |
Script management flaws
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#324 |
Script management very slow on some platforms
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#335 |
Script management: old-style undo broken in Isar
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#245 |
Script management: parsing protocol error
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#110 |
Search Rewrite and Search About queries for Proof General/Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#345 |
Semi-colons (';') cause outer syntax error: one command expected
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#453 |
Sending too-large definitions gets stuck
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#200 |
Sledgehammer output broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#347 |
Slight change in proof-store-buffer-win to enable undo in the Notepad
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#452 |
Some Isabelle options enabled but not active
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#503 |
Some coq output get lost for query processed just after an error stops the queue.
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#468 |
Some notations with periods make PG hang
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#271 |
Special characters in Isabelle identifiers missing?
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#206 |
Special markup not processed in minibuffer messages (warnings etc.)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#325 |
Splash buffer occupies half the frame
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.0
|
2:pg-emacs
|
#288 |
Splash screen misbehaves
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#36 |
Split stream for console into input/output and give input a different colour.
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#114 |
Spurious "replaced xyz occurrences" messages
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#436 |
Starting the coq process results in an error
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#438 |
Startup failure on Emacs 23
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#323 |
Strange errors of make compile concerning save-excursion/set-buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#181 |
Strange font-lock warning/error in GNU Emacs 21.4.1 (Ubuntu 7.10)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#328 |
Strange resizing of main buffer after minibuffer dialog corres
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#326 |
Strange warnings on Emacs for Mac OS X
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#180 |
Sub/superscript sometimes not rendered properly.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#310 |
Subscripts in locked region are revealed the moment you finish a lemma
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#341 |
Suggestion to recover the default C-h suffix for Emacs keys help
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#48 |
Support editing proof script files outside workspace
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#422 |
Support for entering ellipsis in electric terminator mode
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#293 |
Synchronisation losses with undo-on-edit
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#379 |
Syntax error in ProofGeneral.desktop file
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#467 |
The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof
|
hendrik
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#161 |
The font-lock setup misbehaves when started via menu
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#216 |
Toolbar size on Carbon Emacs
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#1 |
Try to get trac working for Proof General web
|
David Aspinall
|
enhancement
|
major
|
|
6:web-and-docs
|
#316 |
UI glitch: point still jumps about when follow-mode=never move
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#301 |
Ubuntu 9.10: PG menus broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#174 |
Unable to exit prover
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#290 |
Undo and delete for token input don't behave as expected
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#189 |
Undo does not work for diagnostic commands in proofs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#295 |
Undo on edit in ML-sections
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#352 |
Unexpected shift in toolbar buttons
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#280 |
Unicode Tokens: cleanups
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#312 |
Unicode tokens: add support for PhoX
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#311 |
Unicode tokens: cannot select certain fonts from menu
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#313 |
Unicode tokens: tweak support for Coq
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#329 |
Unwanted kill-buffer at startup
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#222 |
Urgent messages override errors
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#4 |
Use stixfonts once they become available
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
1:pg-eclipse
|
#440 |
User manual link on development page broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#463 |
Warning messages suppress error messages and make PG have incorrect behavior with Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#141 |
Warnings missing in proof mode in Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#417 |
Website states wrong minimal emacs version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
6:web-and-docs
|
#415 |
Wrong file mentioned in installation notes
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
6:web-and-docs
|
#129 |
X-Symbol in GNU Emacs: fix support for hiding tokens \<^loc>, \<bsub>, etc
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#224 |
X-Symbol on Carbon Emacs 1.6.0: problem with sub/superscripts
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#201 |
X-Symbol only half enabled (Emacs: yes, prover: no)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#221 |
XEmacs 21.4.x: Isabelle logic menu broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#484 |
[Existing Instances] should be highlighted like [Existing Instance]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#476 |
[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#478 |
[Proof <body term>.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#477 |
[Proposition] is not highlighted like [Lemma]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#475 |
[exists] tactic causes improper indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#479 |
[intros ??.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#482 |
[lazymatch] should be highlighted and indented like [match]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#223 |
\<zero> vs. \<one> tokens
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#254 |
a spam ticket
|
Graham Dutton
|
defect
|
major
|
|
2:pg-emacs
|
#283 |
assert command etc.: strange movement of point
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#400 |
assert newly added text in ancestor fails
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#406 |
auto compile bugs when some outputs is done by coqc
|
coquser
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|