#76 |
Add Prove-As-You-Type option
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#79 |
Improve symbols: support table inclusions; add Mac and Windows overrides
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#80 |
Improve symbols/character display: allow superscript, subscript (and maybe bold, italic, colours, ...)
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#85 |
Outline view improvements
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#87 |
Add support for indentation in proof script editor
|
new
|
Graham Dutton
|
enhancement
|
major
|
|
#94 |
Selecting print mode via interface
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#96 |
Start/stop quiet: disable these and use statedisplay instead
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#101 |
Add scriptreplace and menu choice interaction
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#107 |
Support text file searching with symbol encoding/decoding
|
new
|
Graham Dutton
|
enhancement
|
minor
|
|
#108 |
Support proof object searching via search dialog
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#122 |
Use Batch Build Command and Project Batch Build Command
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#125 |
Use <askprefs> message to configure prover-specific preferences
|
new
|
Graham Dutton
|
enhancement
|
major
|
|
#130 |
Add project batch builder
|
new
|
Graham Dutton
|
enhancement
|
minor
|
|
#133 |
Enhance proof project nature: add proof project preference, use prover-specifics
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#134 |
Generalise lexing to better match Isar syntax
|
assigned
|
David Aspinall
|
enhancement
|
major
|
|
#136 |
Add compare support for proof scripts
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#144 |
Build a hybrid top level that removes PG specific one
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#145 |
PGIP parser: add string tokens for categories
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#146 |
Add "sendback" messages to match behaviour added to PG Emacs
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#147 |
Add support for (static) code templates inside Isabelle
|
new
|
David Aspinall
|
enhancement
|
major
|
|
#158 |
cursor positioning is wrong when sending commands
|
accepted
|
Graham Dutton
|
enhancement
|
minor
|
|
#169 |
Complete buffer history enhancement
|
assigned
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
#195 |
Replace crufty PHP code for interpreting outline mode with some Javascript
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#208 |
Generalise Coq's modeline subgoal counter for other provers
|
accepted
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.3
|
#239 |
Remove reliance on dom4j
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#273 |
next-error functions: document and streamline
|
accepted
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
#429 |
Coq should support *trace* buffer for idtac output
|
reopened
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
#454 |
coq mode: compile before import fails when no .v file
|
assigned
|
hendrik
|
enhancement
|
major
|
PG-Emacs-4.3
|
#488 |
Display of Ltac debugging mode
|
new
|
David Aspinall
|
enhancement
|
minor
|
|
#506 |
Please add Proof IDE support to emacs PG
|
new
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.3
|
#514 |
Emacs org-mode integration
|
new
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.3
|
#3 |
Improve code quality: address J2SE best practices in TPTP analysis
|
new
|
somebody
|
task
|
major
|
|
#25 |
Review in-code TODO and FIXME tasks
|
new
|
David Aspinall
|
task
|
minor
|
|
#34 |
Event processing cleanups
|
assigned
|
David Aspinall
|
task
|
major
|
|
#39 |
Code cleanups: use tag CLEANUP for old code prior to removal
|
new
|
David Aspinall
|
task
|
minor
|
|
#59 |
Remove/check through OLD_BUG_LIST.txt
|
new
|
David Aspinall
|
task
|
minor
|
|
#61 |
Make Proof Objects view into standalone RCP application
|
new
|
David Aspinall
|
task
|
minor
|
|
#64 |
Decide what to do with ProverStandalone
|
new
|
alex heneveld
|
task
|
minor
|
|
#65 |
Use FindBugs to detect possible bugs
|
new
|
David Aspinall
|
task
|
major
|
|
#81 |
Investigate use of Computer Modern Unicode font
|
new
|
David Aspinall
|
task
|
minor
|
|
#82 |
Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and isabellesym.sty
|
new
|
David Aspinall
|
task
|
minor
|
|
#132 |
Packaging for 1.0.6/3.4 releases
|
new
|
Graham Dutton
|
task
|
major
|
|
#276 |
Unicode tokens: resolve font-lock issues, optimise
|
accepted
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.3
|
#361 |
Generic adjustment of prover's pretty-printing width
|
accepted
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.3
|
#364 |
Unify proof-query-identifier and pg-identifier-near-point-query (cleanup)
|
accepted
|
David Aspinall
|
task
|
trivial
|
PG-Emacs-4.3
|
#367 |
Fix web pages and update screenshots
|
accepted
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.3
|
#425 |
Consider simplifying span amalgamation to match prover undo behaviour
|
accepted
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.3
|
#457 |
Remove/invoke proof-shell-pre-interrupt-hook
|
new
|
David Aspinall
|
task
|
minor
|
PG-Emacs-4.3
|
#249 |
Script management error for locales; undo action failure should not generate markers
|
assigned
|
David Aspinall
|
|
critical
|
|