#319 |
delete would be nice if it didn't expant symbols
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#320 |
Processing currently gobbles comments and white space: better if it didn't
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#321 |
Retract buffer broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#322 |
Isabelle: "error in process filter: Wrong number of arguments" when using tracing() in ML
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#324 |
Script management very slow on some platforms
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#325 |
Splash buffer occupies half the frame
|
David Aspinall
|
defect
|
trivial
|
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
|
#327 |
Elisp stack overflow when retracting many files at once
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#328 |
Strange resizing of main buffer after minibuffer dialog corres
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#329 |
Unwanted kill-buffer at startup
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#330 |
Error raised by proof-issue-goal and proof-issue-save
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#331 |
Coq config for proof-goal-command and proof-save-command
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#332 |
Minibuffer display of first line of urgent messages lost?
|
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
|
#334 |
Broken Keybindings for Show Me -> ... and others
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#335 |
Script management: old-style undo broken in Isar
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#337 |
C-c C-a h is undefined
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#339 |
Infinite loop on module print with coq-8.3
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#340 |
Key binding syntax in proof-splash.el
|
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
|
#342 |
Distracting error (actually raised by coq-command-at-point)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#343 |
Missing test in proof-store-buffer-win
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#344 |
proof-retract-buffer incomplete
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#345 |
Semi-colons (';') cause outer syntax error: one command expected
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#346 |
Coq multiple keywords are wrongly colorized
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#348 |
Need to update in coq-syntax.el the keywords containing the word Local
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#349 |
proof-process-buffer in a single shot (Mac OS X)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#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
|
#352 |
Unexpected shift in toolbar buttons
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#355 |
Autosend should be re-engaged after C-c C-n
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#356 |
Coq identifiers are unexpectedly colorized
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#357 |
Feature suggestion: function + binding to insert Coq closing tactics
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.1
|
7:prover-coq
|
#358 |
link to proof general is broken
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#359 |
Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & coq-SearchAbout)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#360 |
link to proof general is broken and lacks helpful message
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#362 |
Proof Completed message for Coq is lost
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#363 |
Multiple file handling for Coq needs sensible treatment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#365 |
Fix three mouse bindings in proof-menu.el, pg-goals.el, and pg-vars.el
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#366 |
Fix documentation for mouse button commands
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#368 |
coq, already defined values
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
7:prover-coq
|
#369 |
PG will not compile under non-windowing Emacs
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#370 |
Proof General immediately starts processing the file as soon as I open it
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#371 |
electric terminator mode broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#372 |
funny => sign all over my scripts
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#373 |
PG 4.0 forgets things.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#374 |
cannot turn on electric-terminator interactively
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#375 |
PG goes into infinite loop with 100% CPU usage
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#376 |
Enable and complete testing of parser cache, add to user options menu
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#378 |
Makefile "make" should detect wrong bytecode file version and rebuild
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#379 |
Syntax error in ProofGeneral.desktop file
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#380 |
Downloaded bytecode buggy?
|
David Aspinall
|
defect
|
major
|
|
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
|
#382 |
coq-mode inhibits automatic saving of abbrevs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
7:prover-coq
|
#383 |
no deactivation-hooks when killing fully asserted active buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#384 |
Isabelle process killed rudely
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#387 |
Preferences lost when prover restarted
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#389 |
Mac OS X font selection problems
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#390 |
Odd progress markers in text mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#391 |
proof-full-annotation causes instabilities
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#392 |
Isabelle anti-quotation colouring obliterates symbol font setting
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#395 |
proof-segment-up-to-using-cache broken since Oct 11 20:07:17 2010 +0200
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#396 |
error in proof-shell-insert-hook docstring
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#397 |
Coq PG: changing scripting buffer and automatically restarting misses first command
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#398 |
Compilation failure with mmm and Emacs development version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#399 |
dvi target in doc/Makefile.doc missing
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#400 |
assert newly added text in ancestor fails
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#402 |
Clean up customization groups/settings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#403 |
comment-dwim and kill-rectangle in the locked region
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#404 |
Coq parse error with undelimited comment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#405 |
Report Emacs bug: Quail input breaks delete-char behaviour
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#407 |
proof-undo-and-delete-last-successful-command does not meet spec
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#408 |
Auto compile fails if coq-compile-response-buffer has been killed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#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
|
#411 |
wiki formatting corrupts tickets
|
David Aspinall
|
defect
|
minor
|
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
|
#414 |
PG thinks Preterm command is not state-preserving
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#415 |
Wrong file mentioned in installation notes
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
6:web-and-docs
|
#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
|
#419 |
Print Fully Explicit option gets out of sync after undoing before point where it was changed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
7:prover-coq
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#422 |
Support for entering ellipsis in electric terminator mode
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#423 |
List customisation variables use wrong widget
|
David Aspinall
|
defect
|
minor
|
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
|
#427 |
defpacustom and undo
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#428 |
subsubsection links not working in PG doc
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#430 |
Make "Set Ltac Debug" work
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#431 |
"This subproof is complete" appears at bottom of goals
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.2
|
7:prover-coq
|
#432 |
Add documentation of *trace* buffer to PG Adapting manual
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#433 |
unexpected cursor position after stepping through command with terminator at line ending
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.3
|
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
|