#24 |
Replace current undo management with document-based undo mechanism
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#84 |
Remove double-quoted XML output from term display
|
David Aspinall
|
defect
|
blocker
|
|
4:prover-isabelle
|
#86 |
Fix parse edit offset
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#124 |
Edited text doesn't update document model
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#126 |
Repair symbol handling
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#156 |
closing an active editor doesn't work (buggy or confusing PGRetargetableAction.setBusy())
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#220 |
Remove X-Symbol, XEmacs support and backward compatibility
|
David Aspinall
|
task
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#241 |
Fix link parse and undo for <whitespace> elements.
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#245 |
Script management: parsing protocol error
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#358 |
link to proof general is broken
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#360 |
link to proof general is broken and lacks helpful message
|
David Aspinall
|
defect
|
blocker
|
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
|
#375 |
PG goes into infinite loop with 100% CPU usage
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#469 |
coqgeneral 4.3pre130327 does not compile with Emacs 24.3
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.3
|
2:pg-emacs
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.3
|
2:pg-emacs
|
#511 |
new Coq command "From" supported by PG?
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.4
|
2:pg-emacs
|
#83 |
Fix script parsing to produce reliable and speedy <parseresult> outputs
|
David Aspinall
|
defect
|
critical
|
|
4:prover-isabelle
|
#139 |
Prover not started when run from Product
|
Graham Dutton
|
defect
|
critical
|
|
1:pg-eclipse
|
#157 |
undo sometimes incorrectly tries to undo a larger container than is appropriate
|
David Aspinall
|
defect
|
critical
|
|
1:pg-eclipse
|
#406 |
auto compile bugs when some outputs is done by coqc
|
coquser
|
defect
|
critical
|
PG-Emacs-4.2
|
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
|
#428 |
subsubsection links not working in PG doc
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.3
|
2:pg-emacs
|
#1 |
Try to get trac working for Proof General web
|
David Aspinall
|
enhancement
|
major
|
|
6:web-and-docs
|
#4 |
Use stixfonts once they become available
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
1:pg-eclipse
|
#6 |
Add code folding for proof scripts
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#7 |
Finish proof explorer: inherit decorators, menus, etc. from Project Explorer.
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#16 |
Move cursor and scroll during do/undo
|
Graham Dutton
|
defect
|
major
|
|
1:pg-eclipse
|
#20 |
Fix ProofScriptEditor to change symbols cleanly
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#50 |
Make sure PG perspective is default on product startup.
|
David Aspinall
|
defect
|
major
|
|
documentation
|
#56 |
PGActions do not always clear their status (report "someone else owns the prover")
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#63 |
Improve symbols: fill out default table, add ascii-symbol completion
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#68 |
Move to Eclipse 3.3 at 3.3M5
|
David Aspinall
|
task
|
major
|
|
1:pg-eclipse
|
#70 |
Add documentation for developer-recommended plugins
|
David Aspinall
|
task
|
major
|
|
6:web-and-docs
|
#71 |
Add Error Decoration to documents; optimise Active Script Decoration
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#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
|
#88 |
Buffer invisibility spec bug with Emacs 22
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#91 |
PGML: add markup for subscript, superscript, bold, ...
|
David Aspinall
|
defect
|
major
|
|
5:PGIP-design
|
#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
|
#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
|
#118 |
Complete X-Symbol unicode patch and add symbol configuration for Isabelle
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7.1
|
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
|
#128 |
Navigator view broken
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#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
|
#140 |
PG takes a long time printing module types in Coq
|
courtieu
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#141 |
Warnings missing in proof mode in Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#143 |
Add XML/PGIP test scripts to Isabelle/Admin distribution
|
David Aspinall
|
enhancement
|
major
|
|
4:prover-isabelle
|
#152 |
Faults with main regexps in XEmacs 21.5(b28) for Coq
|
courtieu
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#154 |
"restart" doesn't work
|
alex heneveld
|
defect
|
major
|
|
1:pg-eclipse
|
#161 |
The font-lock setup misbehaves when started via menu
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#162 |
Compatibility ProofGeneral-3.7pre071025, Isabelle, XEmacs 21.5.28
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#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
|
#164 |
Error with GNU Emacs 21.4.1/C-c C-BS
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#165 |
Cygwin: font-lock crashes on XEmacs 21.4.20
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#166 |
Out of sync on illegal escape character
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#177 |
Complete Unicode Token coding system and input method
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#178 |
Emacs occasionally hangs when doing isearch-forward.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#179 |
Losing sync with interrupt
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#180 |
Sub/superscript sometimes not rendered properly.
|
David Aspinall
|
defect
|
major
|
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
|
#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
|
#189 |
Undo does not work for diagnostic commands in proofs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7
|
4:prover-isabelle
|
#193 |
Fix output of texi2html
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
6:web-and-docs
|
#196 |
Fix X-Symbol for Emacs 23
|
David Aspinall
|
defect
|
major
|
|
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
|
#203 |
Carbon Emacs: no colouring of variables in Isabelle output
|
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
|
#205 |
x-symbol fails in Carbon Emacs
|
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
|
#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
|
#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
|
#218 |
Add documentation for Isabelle settings
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.0
|
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
|
#222 |
Urgent messages override errors
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#223 |
\<zero> vs. \<one> tokens
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#224 |
X-Symbol on Carbon Emacs 1.6.0: problem with sub/superscripts
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|
#232 |
Add documentation for Unicode Tokens mode
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.0
|
2:pg-emacs
|
#233 |
Coq fails to start
|
David Aspinall
|
defect
|
major
|
PG-Emacs-3.7.1
|
2:pg-emacs
|