#160 |
"Abort" keyword not recognized in Coq
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#431 |
"This subproof is complete" appears at bottom of goals
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.2
|
7:prover-coq
|
#485 |
"Time commands" option offsets the cursor when errors are reported
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#154 |
"restart" doesn't work
|
alex heneveld
|
defect
|
major
|
|
1:pg-eclipse
|
#309 |
-p option (Isar interface) does not permit additional parameters to emacs executable
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
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
|
#103 |
Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7
|
7:prover-coq
|
#71 |
Add Error Decoration to documents; optimise Active Script Decoration
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#143 |
Add XML/PGIP test scripts to Isabelle/Admin distribution
|
David Aspinall
|
enhancement
|
major
|
|
4:prover-isabelle
|
#6 |
Add code folding for proof scripts
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#226 |
Add configurable key bindings to Unicode Tokens tables
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#218 |
Add documentation for Isabelle settings
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#232 |
Add documentation for Unicode Tokens mode
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#70 |
Add documentation for developer-recommended plugins
|
David Aspinall
|
task
|
major
|
|
6:web-and-docs
|
#432 |
Add documentation of *trace* buffer to PG Adapting manual
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#121 |
Add download counter to web
|
Graham Dutton
|
enhancement
|
major
|
PG-Emacs-3.7
|
6:web-and-docs
|
#137 |
Add output highlighting/insert support for Isar and sledgehammer ("Sendback")
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#131 |
Add preference setting for interrupt command
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#117 |
Add resized toolbar icons
|
David Aspinall
|
task
|
minor
|
PG-Emacs-3.7
|
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
|
#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
|
#199 |
Allow use of Isabelle.command to wrap commands singly
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#52 |
An issue with current version of Trac
|
David Aspinall
|
defect
|
minor
|
|
6:web-and-docs
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#269 |
Aquamacs key bindings don't work
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#92 |
Attempt recovery from XML parse errors in PGIP main loop
|
David Aspinall
|
defect
|
minor
|
|
4:prover-isabelle
|
#408 |
Auto compile fails if coq-compile-response-buffer has been killed
|
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
|
#334 |
Broken Keybindings for Show Me -> ... and others
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#88 |
Buffer invisibility spec bug with Emacs 22
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#500 |
Build fails, due to “'isar-markup-ml' is not known to be defined.” (PG 4.2, Mac OS 10.10.2, Aquamacs 3.2)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
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
|
#337 |
C-c C-a h is undefined
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#459 |
Can not split the window vertically
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#138 |
Can't insert text after locking a comment
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#265 |
Cannot open load file: easymenu
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#203 |
Carbon Emacs: no colouring of variables in Isabelle output
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#212 |
Carbon Emacs: strange unicode abbreviations
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#213 |
Carbon Emacs: strange unicode abbreviations
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#111 |
Centering the goal window on the right part of the goals
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#217 |
Chosen logic: changes should invoke isabelle-load-isar-keywords
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#402 |
Clean up customization groups/settings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#8 |
Cleanup active script handling in actions
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#248 |
Clear error markers at correct points (e.g., when processing text successfully)
|
Graham Dutton
|
|
major
|
|
1:pg-eclipse
|
#413 |
Clicking on Find icon does not bring up input buffer
|
David Aspinall
|
defect
|
major
|
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
|
#162 |
Compatibility ProofGeneral-3.7pre071025, Isabelle, XEmacs 21.5.28
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#398 |
Compilation failure with mmm and Emacs development version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#177 |
Complete Unicode Token coding system and input method
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#118 |
Complete X-Symbol unicode patch and add symbol configuration for Isabelle
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#15 |
Concurrency fixes in GetCommandResponseAction
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#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
|
#258 |
Copying from response buffer also copies colour control chars
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#394 |
Coq "Library" keyword - incorrect coloring
|
courtieu
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#211 |
Coq : deactivation of the 'Holes' functionality
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
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
|
#113 |
Coq commands not described in coq/coq-syntax.el
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
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
|
#233 |
Coq fails to start
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.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
|
#356 |
Coq identifiers are unexpectedly colorized
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#302 |
Coq mode requires hilit19.el which is not in Emacs 23
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#346 |
Coq multiple keywords are wrongly colorized
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#404 |
Coq parse error with undelimited comment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
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
|
#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
|
#236 |
Crash when entering antiquotation
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#165 |
Cygwin: font-lock crashes on XEmacs 21.4.20
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#486 |
Disable long indention under quantifiers?
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
3:pg-broker
|
#342 |
Distracting error (actually raised by coq-command-at-point)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#171 |
Documentation fix for Isabelle keybindings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
6:web-and-docs
|
#380 |
Downloaded bytecode buggy?
|
David Aspinall
|
defect
|
major
|
|
2:pg-emacs
|
#289 |
Drawback of command wrapping in PG+Isar
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#314 |
Duplication of some special messages
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#124 |
Edited text doesn't update document model
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#327 |
Elisp stack overflow when retracting many files at once
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#300 |
Emacs 22: strange keyword categorization
|
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
|
#282 |
Emacs 23.1.1 on Mac OS: no toolbar
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#215 |
Emacs 23: toolbar issues
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#235 |
Emacs forgets unicode tokens option
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#416 |
Emacs indentation can go into an infinite loop
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#418 |
Emacs is not responding after typing `Case "".<newline>`
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#178 |
Emacs occasionally hangs when doing isearch-forward.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
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
|
#376 |
Enable and complete testing of parser cache, add to user options menu
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.1
|
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
|
#164 |
Error with GNU Emacs 21.4.1/C-c C-BS
|
David Aspinall
|
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
|
#152 |
Faults with main regexps in XEmacs 21.5(b28) for Coq
|
courtieu
|
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
|
#112 |
Filter out control characters in shell buffer or copy from shell buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#297 |
Finding of lisp relative to the "proofgeneral" script is broken
|
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
|