#296 |
PG accepts garbage though Coq said "illegal begin of vernac"
|
courtieu
|
defect
|
major
|
PG-Emacs-4.2
|
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
|
#378 |
Makefile "make" should detect wrong bytecode file version and rebuild
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.2
|
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
|
#402 |
Clean up customization groups/settings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#405 |
Report Emacs bug: Quail input breaks delete-char behaviour
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#406 |
auto compile bugs when some outputs is done by coqc
|
coquser
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#409 |
Problem with wide unicode characters in emacs 23.3
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
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
|
#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
|
#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
|
#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
|
#453 |
Sending too-large definitions gets stuck
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#168 |
Reorganise TODO files in distribution
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#190 |
Improve proof shell initialisation order
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.1
|
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
|
#217 |
Chosen logic: changes should invoke isabelle-load-isar-keywords
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#226 |
Add configurable key bindings to Unicode Tokens tables
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#228 |
Restore tracing slow mode if necessary
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
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
|
#279 |
Proof visibility controls broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#289 |
Drawback of command wrapping in PG+Isar
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#290 |
Undo and delete for token input don't behave as expected
|
David Aspinall
|
defect
|
major
|
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
|
#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
|
#308 |
Emacs 23 slow -- especially on Cygwin
|
David Aspinall
|
defect
|
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
|
#312 |
Unicode tokens: add support for PhoX
|
David Aspinall
|
task
|
major
|
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
|
#318 |
Report emacs bug: segfault with use of display property/font-lock
|
David Aspinall
|
task
|
major
|
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
|
#324 |
Script management very slow on some platforms
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
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
|
#345 |
Semi-colons (';') cause outer syntax error: one command expected
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
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
|
#357 |
Feature suggestion: function + binding to insert Coq closing tactics
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.1
|
7:prover-coq
|
#363 |
Multiple file handling for Coq needs sensible treatment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#371 |
electric terminator mode broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
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
|
#379 |
Syntax error in ProofGeneral.desktop file
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
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
|
#386 |
Coq goals counter not reset on backtracking out of proof
|
courtieu
|
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
|
#394 |
Coq "Library" keyword - incorrect coloring
|
courtieu
|
defect
|
trivial
|
PG-Emacs-4.1
|
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
|
#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
|
#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
|
#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
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#421 |
proof-shell-exit raises an exception "Buffer foo.v has no process"
|
coquser
|
defect
|
critical
|
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
|
#137 |
Add output highlighting/insert support for Isar and sledgehammer ("Sendback")
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#140 |
PG takes a long time printing module types in Coq
|
courtieu
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#166 |
Out of sync on illegal escape character
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#170 |
Improve outline syntax for Isar
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#177 |
Complete Unicode Token coding system and input method
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#179 |
Losing sync with interrupt
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#187 |
If sent command fails, don't move the cursor.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|