#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
|
#8 |
Cleanup active script handling in actions
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#15 |
Concurrency fixes in GetCommandResponseAction
|
David Aspinall
|
defect
|
minor
|
|
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
|
#24 |
Replace current undo management with document-based undo mechanism
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#28 |
Newlines in PGIP console are lost
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#30 |
Outline view should update after any parse
|
Graham Dutton
|
defect
|
minor
|
|
1:pg-eclipse
|
#36 |
Split stream for console into input/output and give input a different colour.
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#48 |
Support editing proof script files outside workspace
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#49 |
Make sure File->Open produces sensible feedback when attempted with script files
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#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
|
#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
|
#69 |
PGMarkerMethods: skip spaces in document before error marker start
|
Graham Dutton
|
defect
|
minor
|
|
1:pg-eclipse
|
#71 |
Add Error Decoration to documents; optimise Active Script Decoration
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#78 |
Preferences: support dynamically computed defaults
|
David Aspinall
|
enhancement
|
trivial
|
|
1:pg-eclipse
|
#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
|
#128 |
Navigator view broken
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#131 |
Add preference setting for interrupt command
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#139 |
Prover not started when run from Product
|
Graham Dutton
|
defect
|
critical
|
|
1:pg-eclipse
|
#153 |
is "proof state" view needed anymore?
|
David Aspinall
|
task
|
minor
|
|
1:pg-eclipse
|
#154 |
"restart" doesn't work
|
alex heneveld
|
defect
|
major
|
|
1:pg-eclipse
|
#155 |
sending past end doesn't work quite right ("undo" fails, maybe more)
|
David Aspinall
|
defect
|
minor
|
|
1:pg-eclipse
|
#156 |
closing an active editor doesn't work (buggy or confusing PGRetargetableAction.setBusy())
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#157 |
undo sometimes incorrectly tries to undo a larger container than is appropriate
|
David Aspinall
|
defect
|
critical
|
|
1:pg-eclipse
|
#238 |
Remove goto thread
|
Graham Dutton
|
defect
|
major
|
|
1:pg-eclipse
|
#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
|
#245 |
Script management: parsing protocol error
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#248 |
Clear error markers at correct points (e.g., when processing text successfully)
|
Graham Dutton
|
|
major
|
|
1:pg-eclipse
|
#253 |
Refactor to allow more converter objects, investigate conversion mechanisms
|
David Aspinall
|
defect
|
major
|
|
1:pg-eclipse
|
#259 |
Parsing Failure at ends of files
|
Graham Dutton
|
defect
|
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
|
#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
|
#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
|
#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
|
#137 |
Add output highlighting/insert support for Isar and sledgehammer ("Sendback")
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#138 |
Can't insert text after locking a comment
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
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
|
#152 |
Faults with main regexps in XEmacs 21.5(b28) for Coq
|
courtieu
|
defect
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|
#159 |
Goal centering
|
courtieu
|
enhancement
|
minor
|
PG-Emacs-4.2
|
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
|
#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
|
#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
|
#168 |
Reorganise TODO files in distribution
|
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
|
#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
|
#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
|
#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
|
#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
|
#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
|
#187 |
If sent command fails, don't move the cursor.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#188 |
Option to treat comments as individual statements.
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#190 |
Improve proof shell initialisation order
|
David Aspinall
|
task
|
minor
|
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
|
#192 |
Improve out-of-the-box behaviour for some common configurations
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#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
|
#199 |
Allow use of Isabelle.command to wrap commands singly
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
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
|
#211 |
Coq : deactivation of the 'Holes' functionality
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|