#28 |
Newlines in PGIP console are lost
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#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
|
#128 |
Navigator view broken
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#363 |
Multiple file handling for Coq needs sensible treatment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#67 |
Move to Java 6...
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.3
|
1:pg-eclipse
|
#68 |
Move to Eclipse 3.3 at 3.3M5
|
David Aspinall
|
task
|
major
|
|
1:pg-eclipse
|
#16 |
Move cursor and scroll during do/undo
|
Graham Dutton
|
defect
|
major
|
|
1:pg-eclipse
|
#343 |
Missing test in proof-store-buffer-win
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#109 |
Missing output from Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#504 |
Minor fix for coq-is-symbol-or-punct and coq-grab-punctuation-left
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#332 |
Minibuffer display of first line of urgent messages lost?
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#274 |
Max lisp nesting exceeded on large error outputs
|
Makarius
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#50 |
Make sure PG perspective is default on product startup.
|
David Aspinall
|
defect
|
major
|
|
documentation
|
#49 |
Make sure File->Open produces sensible feedback when attempted with script files
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#294 |
Make pg-protected-undo allow in undo in comments of locked region
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#430 |
Make "Set Ltac Debug" work
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#389 |
Mac OS X font selection problems
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#179 |
Losing sync with interrupt
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#423 |
List customisation variables use wrong widget
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#266 |
Limited hilite markup (in Isabelle)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.3
|
2:pg-emacs
|
#340 |
Key binding syntax in proof-splash.el
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#304 |
Isabelle: trying to undo a step fails for me
|
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
|
#267 |
Isabelle sendback markup dysfunctional
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#384 |
Isabelle process killed rudely
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#298 |
Isabelle indentation
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#115 |
Isabelle find-theorems form
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#392 |
Isabelle anti-quotation colouring obliterates symbol font setting
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#339 |
Infinite loop on module print with coq-8.3
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#474 |
Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#473 |
Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#63 |
Improve symbols: fill out default table, add ascii-symbol completion
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#190 |
Improve proof shell initialisation order
|
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
|
#192 |
Improve out-of-the-box behaviour for some common configurations
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#187 |
If sent command fails, don't move the cursor.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#305 |
High overhead
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#268 |
Hiding proofs wrong with Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#439 |
Hang on open bracket
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
7:prover-coq
|
#495 |
Goals buffer aggressively cleared with Coq pre-8.5
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#159 |
Goal centering
|
courtieu
|
enhancement
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#292 |
Goal buffer not updated on "undo" and "goto
|
David Aspinall
|
defect
|
major
|
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
|
#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
|
#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
|
#83 |
Fix script parsing to produce reliable and speedy <parseresult> outputs
|
David Aspinall
|
defect
|
critical
|
|
4:prover-isabelle
|
#219 |
Fix path loading for docstring magic in ProofGeneral.texi
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#86 |
Fix parse edit offset
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#193 |
Fix output of texi2html
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
6:web-and-docs
|
#241 |
Fix link parse and undo for <whitespace> elements.
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#242 |
Fix intro configuration (welcome page)
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#505 |
Fix indentation of lazymatch in Coq
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#366 |
Fix documentation for mouse button commands
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#120 |
Fix docstring magic to interpret blank lines as whitespace inside verbatim regions
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
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
|
#119 |
Fix compilation problems, missing files
|
courtieu
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#196 |
Fix X-Symbol for Emacs 23
|
David Aspinall
|
defect
|
major
|
|
2:pg-emacs
|
#20 |
Fix ProofScriptEditor to change symbols cleanly
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#261 |
Finish support for proof-query-identifier
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#7 |
Finish proof explorer: inherit decorators, menus, etc. from Project Explorer.
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#297 |
Finding of lisp relative to the "proofgeneral" script is broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#112 |
Filter out control characters in shell buffer or copy from shell buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#357 |
Feature suggestion: function + binding to insert Coq closing tactics
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.1
|
7:prover-coq
|
#152 |
Faults with main regexps in XEmacs 21.5(b28) for Coq
|
courtieu
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#185 |
Failed initialization of *trace* buffer (xemacs-21.4.x)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#186 |
Failed initialization of *trace* buffer (xemacs-21.4.x)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#164 |
Error with GNU Emacs 21.4.1/C-c C-BS
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
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
|
#376 |
Enable and complete testing of parser cache, add to user options menu
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.1
|
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
|
#178 |
Emacs occasionally hangs when doing isearch-forward.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#418 |
Emacs is not responding after typing `Case "".<newline>`
|
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
|
#235 |
Emacs forgets unicode tokens option
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#215 |
Emacs 23: toolbar issues
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#282 |
Emacs 23.1.1 on Mac OS: no toolbar
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#308 |
Emacs 23 slow -- especially on Cygwin
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#300 |
Emacs 22: strange keyword categorization
|
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
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#124 |
Edited text doesn't update document model
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#314 |
Duplication of some special messages
|
David Aspinall
|
defect
|
major
|
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
|
#380 |
Downloaded bytecode buggy?
|
David Aspinall
|
defect
|
major
|
|
2:pg-emacs
|
#171 |
Documentation fix for Isabelle keybindings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
6:web-and-docs
|
#342 |
Distracting error (actually raised by coq-command-at-point)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#486 |
Disable long indention under quantifiers?
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
3:pg-broker
|
#165 |
Cygwin: font-lock crashes on XEmacs 21.4.20
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#209 |
Cursor not visible in *response* buffer (GNU Emacs 22 + Carbon Emacs)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#236 |
Crash when entering antiquotation
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#74 |
Coq: bug in electric terminator: typing '.' in comment causes comment to be sent and locked
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#116 |
Coq syntax highlighting: identifiers starting with "fun" are wrongly coloured
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-3.7
|
2:pg-emacs
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#404 |
Coq parse error with undelimited comment
|
David Aspinall
|
defect
|
major
|
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
|
#302 |
Coq mode requires hilit19.el which is not in Emacs 23
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#356 |
Coq identifiers are unexpectedly colorized
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|