#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
|
#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
|
#369 |
PG will not compile under non-windowing Emacs
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
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
|
#197 |
Non-persistance of Unicode Tokens / Math Menu (Carbon Emacs 1.6.0)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#198 |
Prover executable not found when running without interface script
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#200 |
Sledgehammer output broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#201 |
X-Symbol only half enabled (Emacs: yes, prover: no)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#202 |
Prover chokes on Unicode Tokens (Carbon Emacs)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#204 |
undo stops undoing in large proofs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#206 |
Special markup not processed in minibuffer messages (warnings etc.)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#207 |
dir symbol is void on leopard coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
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
|
#210 |
input of symbols in Carbon Emacs
|
David Aspinall
|
enhancement
|
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
|
#214 |
Processing of buffer sensitive to Unicode option
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#215 |
Emacs 23: toolbar issues
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#219 |
Fix path loading for docstring magic in ProofGeneral.texi
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#221 |
XEmacs 21.4.x: Isabelle logic menu broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#223 |
\<zero> vs. \<one> tokens
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#233 |
Coq fails to start
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
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
|
#109 |
Missing output from Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#110 |
Search Rewrite and Search About queries for Proof General/Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
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
|
#112 |
Filter out control characters in shell buffer or copy from shell buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#113 |
Coq commands not described in coq/coq-syntax.el
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#114 |
Spurious "replaced xyz occurrences" messages
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#115 |
Isabelle find-theorems form
|
David Aspinall
|
enhancement
|
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
|
#117 |
Add resized toolbar icons
|
David Aspinall
|
task
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#119 |
Fix compilation problems, missing files
|
courtieu
|
defect
|
major
|
PG-Emacs-3.7
|
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
|
#121 |
Add download counter to web
|
Graham Dutton
|
enhancement
|
major
|
PG-Emacs-3.7
|
6:web-and-docs
|
#129 |
X-Symbol in GNU Emacs: fix support for hiding tokens \<^loc>, \<bsub>, etc
|
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
|
#160 |
"Abort" keyword not recognized in Coq
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#161 |
The font-lock setup misbehaves when started via menu
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#163 |
Problems with x-symbol in XEmacs 21.5.28 (latin-iso8859-2 error)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#171 |
Documentation fix for Isabelle keybindings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
6:web-and-docs
|
#172 |
Problem with indentation in Coq mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#173 |
coq indenting mode gets confused by *) in proofs
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#174 |
Unable to exit prover
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#175 |
ProofGeneral accidentally resets itself while scrolling
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#180 |
Sub/superscript sometimes not rendered properly.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#181 |
Strange font-lock warning/error in GNU Emacs 21.4.1 (Ubuntu 7.10)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-3.7
|
2:pg-emacs
|
#182 |
Problem with sub/superscript in GNU Emacs 21.4.1 (Ubuntu 7.10)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#183 |
ProofGeneral crashes when displaying tracing messages
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#184 |
lib/maths-menu.el doesn't compile on XEmacs 21.4
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#189 |
Undo does not work for diagnostic commands in proofs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|