#140 |
PG takes a long time printing module types in Coq
|
courtieu
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#137 |
Add output highlighting/insert support for Isar and sledgehammer ("Sendback")
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#166 |
Out of sync on illegal escape character
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#170 |
Improve outline syntax for Isar
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#177 |
Complete Unicode Token coding system and input method
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
fixed
|
#179 |
Losing sync with interrupt
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#187 |
If sent command fails, don't move the cursor.
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#188 |
Option to treat comments as individual statements.
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#191 |
Code cleanup: remove proof-no-command
|
David Aspinall
|
task
|
minor
|
2:pg-emacs
|
fixed
|
#193 |
Fix output of texi2html
|
David Aspinall
|
defect
|
major
|
6:web-and-docs
|
fixed
|
#199 |
Allow use of Isabelle.command to wrap commands singly
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#211 |
Coq : deactivation of the 'Holes' functionality
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#218 |
Add documentation for Isabelle settings
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#220 |
Remove X-Symbol, XEmacs support and backward compatibility
|
David Aspinall
|
task
|
blocker
|
2:pg-emacs
|
fixed
|
#222 |
Urgent messages override errors
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
needmoreinfo
|
#227 |
Recover active scripting modeline indicator
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#229 |
Restore mouse and button actions in goals buffers
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#232 |
Add documentation for Unicode Tokens mode
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
fixed
|
#234 |
unicode-tokens: add command to highlight unicode characters
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
fixed
|
#235 |
Emacs forgets unicode tokens option
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#236 |
Crash when entering antiquotation
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#237 |
Odd behaviour of C-w in script buffers
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
needmoreinfo
|
#257 |
Byte Compilation fails because of comments in the completion file
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
invalid
|
#258 |
Copying from response buffer also copies colour control chars
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#261 |
Finish support for proof-query-identifier
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#262 |
make jobserver unavailable
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#263 |
proof-shell-trace-output-regexp in trace output
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#264 |
GNU Emacs 22.2.1 (SuSE): tty fails
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
worksforme
|
#265 |
Cannot open load file: easymenu
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#266 |
Limited hilite markup (in Isabelle)
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#267 |
Isabelle sendback markup dysfunctional
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#268 |
Hiding proofs wrong with Coq
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#269 |
Aquamacs key bindings don't work
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
needmoreinfo
|
#270 |
Odd PG/Trac link
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#271 |
Special characters in Isabelle identifiers missing?
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#277 |
span start vs. command start
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#278 |
Resolve pointer-movement issues during script management
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#280 |
Unicode Tokens: cleanups
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
fixed
|
#281 |
Odd unicode abbreviations, notably |>
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#282 |
Emacs 23.1.1 on Mac OS: no toolbar
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#283 |
assert command etc.: strange movement of point
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
duplicate
|
#284 |
proof-process-buffer very slow
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#285 |
byte compilation
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#286 |
PG startup crash
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#287 |
Script management flaws
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#288 |
Splash screen misbehaves
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#291 |
3-Panel-mode: Strange buffer switch when loading a theory
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#292 |
Goal buffer not updated on "undo" and "goto
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#297 |
Finding of lisp relative to the "proofgeneral" script is broken
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#298 |
Isabelle indentation
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#299 |
Out of sync with Isabelle
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
needmoreinfo
|
#300 |
Emacs 22: strange keyword categorization
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#301 |
Ubuntu 9.10: PG menus broken
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#302 |
Coq mode requires hilit19.el which is not in Emacs 23
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#303 |
underlining on error sucks
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#304 |
Isabelle: trying to undo a step fails for me
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#305 |
High overhead
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
needmoreinfo
|
#306 |
Odd display of sub/superscripts
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#307 |
synchronization loss with interrupts
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#309 |
-p option (Isar interface) does not permit additional parameters to emacs executable
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#310 |
Subscripts in locked region are revealed the moment you finish a lemma
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#314 |
Duplication of some special messages
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#315 |
failure to show ML errors
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
needmoreinfo
|
#320 |
Processing currently gobbles comments and white space: better if it didn't
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
invalid
|
#321 |
Retract buffer broken
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
needmoreinfo
|
#322 |
Isabelle: "error in process filter: Wrong number of arguments" when using tracing() in ML
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#323 |
Strange errors of make compile concerning save-excursion/set-buffer
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#325 |
Splash buffer occupies half the frame
|
David Aspinall
|
defect
|
trivial
|
2:pg-emacs
|
duplicate
|
#326 |
Strange warnings on Emacs for Mac OS X
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#327 |
Elisp stack overflow when retracting many files at once
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#328 |
Strange resizing of main buffer after minibuffer dialog corres
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
worksforme
|
#329 |
Unwanted kill-buffer at startup
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
duplicate
|
#330 |
Error raised by proof-issue-goal and proof-issue-save
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#331 |
Coq config for proof-goal-command and proof-save-command
|
David Aspinall
|
enhancement
|
minor
|
7:prover-coq
|
fixed
|
#332 |
Minibuffer display of first line of urgent messages lost?
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#333 |
Restart tool button points to manual
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
worksforme
|
#334 |
Broken Keybindings for Show Me -> ... and others
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#335 |
Script management: old-style undo broken in Isar
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
worksforme
|
#337 |
C-c C-a h is undefined
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
duplicate
|
#339 |
Infinite loop on module print with coq-8.3
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#340 |
Key binding syntax in proof-splash.el
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#341 |
Suggestion to recover the default C-h suffix for Emacs keys help
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
fixed
|
#342 |
Distracting error (actually raised by coq-command-at-point)
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#343 |
Missing test in proof-store-buffer-win
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#344 |
proof-retract-buffer incomplete
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#346 |
Coq multiple keywords are wrongly colorized
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#347 |
Slight change in proof-store-buffer-win to enable undo in the Notepad
|
David Aspinall
|
enhancement
|
minor
|
7:prover-coq
|
fixed
|
#348 |
Need to update in coq-syntax.el the keywords containing the word Local
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#349 |
proof-process-buffer in a single shot (Mac OS X)
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
#352 |
Unexpected shift in toolbar buttons
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#356 |
Coq identifiers are unexpectedly colorized
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#358 |
link to proof general is broken
|
David Aspinall
|
defect
|
blocker
|
2:pg-emacs
|
invalid
|
#359 |
Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & coq-SearchAbout)
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#360 |
link to proof general is broken and lacks helpful message
|
David Aspinall
|
defect
|
blocker
|
2:pg-emacs
|
fixed
|
#362 |
Proof Completed message for Coq is lost
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#365 |
Fix three mouse bindings in proof-menu.el, pg-goals.el, and pg-vars.el
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#366 |
Fix documentation for mouse button commands
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#368 |
coq, already defined values
|
David Aspinall
|
defect
|
major
|
7:prover-coq
|
needmoreinfo
|
#369 |
PG will not compile under non-windowing Emacs
|
David Aspinall
|
defect
|
blocker
|
2:pg-emacs
|
fixed
|
#370 |
Proof General immediately starts processing the file as soon as I open it
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
invalid
|
(more results for this group on next page)
|