#514 |
Emacs org-mode integration
|
new
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#513 |
Splash screen disappears too quickly
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.4
|
2:pg-emacs
|
#510 |
coq-time-commands hangs on bullets with Coq-8.5
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#509 |
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#508 |
The option -emacs-U is depracated Proof General should use -emacs instead.
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#507 |
PG for Coq does not interpret quotes within comments like Coq does
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#506 |
Please add Proof IDE support to emacs PG
|
new
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#501 |
wrongly embedded pathname in ProofGeneral-4.3pre150202
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#499 |
delays between coq messages can cause PG to duplicate some
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#497 |
coq auto-compile and spaces in directory names lead to failure
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#496 |
Aquamacs point moving
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#490 |
Bad parsing of .}
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#488 |
Display of Ltac debugging mode
|
new
|
David Aspinall
|
enhancement
|
|
2:pg-emacs
|
#483 |
ltac: and constr: should not affect indentation
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#481 |
proof-set-value does not handle errors in :eval forms of defpacustom
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#480 |
[match]es sometimes screw up indentation
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#465 |
proof script not displayed after startup
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#464 |
proof script not displayed after startup
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#462 |
Improve library bundling
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.4
|
2:pg-emacs
|
#457 |
Remove/invoke proof-shell-pre-interrupt-hook
|
new
|
David Aspinall
|
task
|
PG-Emacs-4.3
|
2:pg-emacs
|
#401 |
Parser cache does not respect fly-past-comments
|
accepted
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#385 |
Isabelle theorem dependencies display broken
|
accepted
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#361 |
Generic adjustment of prover's pretty-printing width
|
accepted
|
David Aspinall
|
task
|
PG-Emacs-4.3
|
2:pg-emacs
|
#354 |
synchronisation lost with "process rest" and "undo"
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#336 |
Toolbar images on Mac Emacsen are super-ugly
|
reopened
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#260 |
Path names with spaces are not decoded property on search path
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#256 |
Use prover-specific Preference Initialisers
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#244 |
Comical giant icons in outline view
|
assigned
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#240 |
Bad behaviour in startup when proof executables (isabelle, isatool) not found
|
assigned
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#239 |
Remove reliance on dom4j
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#208 |
Generalise Coq's modeline subgoal counter for other provers
|
accepted
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#195 |
Replace crufty PHP code for interpreting outline mode with some Javascript
|
new
|
David Aspinall
|
enhancement
|
|
6:web-and-docs
|
#158 |
cursor positioning is wrong when sending commands
|
accepted
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#150 |
Remove use of PGIP message datatypes
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#144 |
Build a hybrid top level that removes PG specific one
|
new
|
David Aspinall
|
enhancement
|
|
4:prover-isabelle
|
#133 |
Enhance proof project nature: add proof project preference, use prover-specifics
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#130 |
Add project batch builder
|
new
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#107 |
Support text file searching with symbol encoding/decoding
|
new
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#105 |
Preference handling refactor: add description text preferences, use those for display, remove ids
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#104 |
Add preference listener to ProofScriptDocument
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#102 |
Simplify message model according to new RNC, change Isabelle to match
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#97 |
Add Pretty.markup to parse tree output
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#96 |
Start/stop quiet: disable these and use statedisplay instead
|
new
|
David Aspinall
|
enhancement
|
|
4:prover-isabelle
|
#95 |
Refine spuriouscmd into two: destructivecmd and diagnosticcmd
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#94 |
Selecting print mode via interface
|
new
|
David Aspinall
|
enhancement
|
|
5:PGIP-design
|
#89 |
Remove tabs from Isabelle source files (theories, at least)
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#85 |
Outline view improvements
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#82 |
Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and isabellesym.sty
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#81 |
Investigate use of Computer Modern Unicode font
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#80 |
Improve symbols/character display: allow superscript, subscript (and maybe bold, italic, colours, ...)
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#72 |
Fix prover state indicator
|
new
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#64 |
Decide what to do with ProverStandalone
|
new
|
alex heneveld
|
task
|
|
1:pg-eclipse
|
#62 |
PGIP console displays messages out-of-order; should allow hiding packets
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#61 |
Make Proof Objects view into standalone RCP application
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#60 |
Improve icons throughout
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#59 |
Remove/check through OLD_BUG_LIST.txt
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#58 |
Hangs during shutdown
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#57 |
Symbol table editor problems: doesn't report correct status, apply is very slow
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#53 |
Re-implement toolbar button enablers
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#51 |
Add processing direction to 'active script' decorator
|
new
|
anonymous
|
enhancement
|
|
1:pg-eclipse
|
#46 |
Extra view for Problem Details
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#43 |
Improve output markup (pgml.xsl)
|
assigned
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#39 |
Code cleanups: use tag CLEANUP for old code prior to removal
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#32 |
Add some user documentation
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#31 |
Decorators not always updated
|
new
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#29 |
Symbol table editing scheme: fix filename and add edit action rather than create
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#25 |
Review in-code TODO and FIXME tasks
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#23 |
Test and refine capabilities/activities
|
new
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#22 |
Refactor SessionManager
|
assigned
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#18 |
Add hover for prover output (on any blue space)
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#17 |
Add clear button for prover output
|
accepted
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#13 |
Add proof object search facilities to IdView
|
assigned
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#12 |
Polish Proof Objects View; Link to Prover Knowledge
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#11 |
Builder for parsing/proving files automatically
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#9 |
Fix history in output view
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|