#409 |
Problem with wide unicode characters in emacs 23.3
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#410 |
coq parsing broken since Jun 04 20:12:40
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#412 |
coq parsing broken since Jun 04 20:12:40 (II)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#413 |
Clicking on Find icon does not bring up input buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#416 |
Emacs indentation can go into an infinite loop
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#417 |
Website states wrong minimal emacs version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
6:web-and-docs
|
#418 |
Emacs is not responding after typing `Case "".<newline>`
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#424 |
proof-shell-exit does not follow standard emacs policy with query-exit.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#426 |
proof-user-options custom group partly broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#430 |
Make "Set Ltac Debug" work
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#432 |
Add documentation of *trace* buffer to PG Adapting manual
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#435 |
wrong behaviour of the period
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#436 |
Starting the coq process results in an error
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#437 |
compilation error with LANG=C
|
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
|
#439 |
Hang on open bracket
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
7:prover-coq
|
#440 |
User manual link on development page broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#441 |
make -C doc magic fails
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
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
|
#444 |
three windows mode at pg start when a warning window
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#445 |
Proof General (or coqtop?) barfs on "Arguments foo / ..."
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#446 |
window-live-p error (coq, aquamacs)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#447 |
Proof General stalls on long Ltac (Coq)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#449 |
coq electric terminator conflict
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#450 |
Proof in proof tree
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#451 |
support {} and bullets in prooftree
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#452 |
Some Isabelle options enabled but not active
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#453 |
Sending too-large definitions gets stuck
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#455 |
Emacs trunk BZR sometimes hangs when using auto fill mode with PG Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
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
|
#459 |
Can not split the window vertically
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#460 |
proof general hanging on Coq Definition in file generated by Why3
|
hendrik
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#461 |
old manuals on website
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
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
|
#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
|
#494 |
PG incorrectly parses the result of [Fail] in some cases
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#512 |
test.coq target doesn't exist
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#8 |
Cleanup active script handling in actions
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#15 |
Concurrency fixes in GetCommandResponseAction
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#28 |
Newlines in PGIP console are lost
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#30 |
Outline view should update after any parse
|
Graham Dutton
|
defect
|
minor
|
|
1:pg-eclipse
|
#36 |
Split stream for console into input/output and give input a different colour.
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#48 |
Support editing proof script files outside workspace
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#49 |
Make sure File->Open produces sensible feedback when attempted with script files
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#52 |
An issue with current version of Trac
|
David Aspinall
|
defect
|
minor
|
|
6:web-and-docs
|
#67 |
Move to Java 6...
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.3
|
1:pg-eclipse
|
#69 |
PGMarkerMethods: skip spaces in document before error marker start
|
Graham Dutton
|
defect
|
minor
|
|
1:pg-eclipse
|
#92 |
Attempt recovery from XML parse errors in PGIP main loop
|
David Aspinall
|
defect
|
minor
|
|
4:prover-isabelle
|
#113 |
Coq commands not described in coq/coq-syntax.el
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#117 |
Add resized toolbar icons
|
David Aspinall
|
task
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#131 |
Add preference setting for interrupt command
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#137 |
Add output highlighting/insert support for Isar and sledgehammer ("Sendback")
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#138 |
Can't insert text after locking a comment
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#153 |
is "proof state" view needed anymore?
|
David Aspinall
|
task
|
minor
|
|
1:pg-eclipse
|
#155 |
sending past end doesn't work quite right ("undo" fails, maybe more)
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#159 |
Goal centering
|
courtieu
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#160 |
"Abort" keyword not recognized in Coq
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#167 |
GNU Emacs 22.1.1 allows only one undo in a row from the toolbar while C-c C-u works
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#168 |
Reorganise TODO files in distribution
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#170 |
Improve outline syntax for Isar
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#171 |
Documentation fix for Isabelle keybindings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
6:web-and-docs
|
#172 |
Problem with indentation in Coq mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#173 |
coq indenting mode gets confused by *) in proofs
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#176 |
Allow isabelle-chosen-logic to be set by variable comment in thy file
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-3.7.1
|
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
|
#187 |
If sent command fails, don't move the cursor.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#188 |
Option to treat comments as individual statements.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#190 |
Improve proof shell initialisation order
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#191 |
Code cleanup: remove proof-no-command
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#192 |
Improve out-of-the-box behaviour for some common configurations
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#199 |
Allow use of Isabelle.command to wrap commands singly
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#211 |
Coq : deactivation of the 'Holes' functionality
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#216 |
Toolbar size on Carbon Emacs
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#217 |
Chosen logic: changes should invoke isabelle-load-isar-keywords
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#225 |
Allow Unicode Tokens to work smoothly for several modes at once
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#226 |
Add configurable key bindings to Unicode Tokens tables
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#227 |
Recover active scripting modeline indicator
|
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
|
#229 |
Restore mouse and button actions in goals buffers
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#230 |
Configuration simplification: unify regexp/function settings
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#231 |
Consider replacing maths-menu for token mode with own version
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#257 |
Byte Compilation fails because of comments in the completion file
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#262 |
make jobserver unavailable
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#264 |
GNU Emacs 22.2.1 (SuSE): tty fails
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#269 |
Aquamacs key bindings don't work
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#272 |
Port identifier completion code from PG Eclipse.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#281 |
Odd unicode abbreviations, notably |>
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#289 |
Drawback of command wrapping in PG+Isar
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#291 |
3-Panel-mode: Strange buffer switch when loading a theory
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#294 |
Make pg-protected-undo allow in undo in comments of locked region
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#295 |
Undo on edit in ML-sections
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#309 |
-p option (Isar interface) does not permit additional parameters to emacs executable
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
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
|
#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
|
#316 |
UI glitch: point still jumps about when follow-mode=never move
|
David Aspinall
|
defect
|
minor
|
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
|
#319 |
delete would be nice if it didn't expant symbols
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|