#354
|
synchronisation lost with "process rest" and "undo"
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 14, 2010
|
#11
|
Builder for parsing/proving files automatically
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 29, 2007
|
#18
|
Add hover for prover output (on any blue space)
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#23
|
Test and refine capabilities/activities
|
1:pg-eclipse
|
|
|
enhancement
|
Graham Dutton
|
new
|
Jan 30, 2007
|
#29
|
Symbol table editing scheme: fix filename and add edit action rather than create
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#32
|
Add some user documentation
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#46
|
Extra view for Problem Details
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#60
|
Improve icons throughout
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 1, 2007
|
#80
|
Improve symbols/character display: allow superscript, subscript (and maybe bold, italic, colours, ...)
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 25, 2007
|
#85
|
Outline view improvements
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 27, 2007
|
#94
|
Selecting print mode via interface
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Mar 10, 2007
|
#96
|
Start/stop quiet: disable these and use statedisplay instead
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Mar 10, 2007
|
#107
|
Support text file searching with symbol encoding/decoding
|
1:pg-eclipse
|
|
|
enhancement
|
Graham Dutton
|
new
|
Mar 18, 2007
|
#130
|
Add project batch builder
|
1:pg-eclipse
|
|
|
enhancement
|
Graham Dutton
|
new
|
Jul 8, 2007
|
#133
|
Enhance proof project nature: add proof project preference, use prover-specifics
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jul 11, 2007
|
#144
|
Build a hybrid top level that removes PG specific one
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Sep 14, 2007
|
#239
|
Remove reliance on dom4j
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Aug 14, 2008
|
#25
|
Review in-code TODO and FIXME tasks
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Jan 30, 2007
|
#39
|
Code cleanups: use tag CLEANUP for old code prior to removal
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Jan 30, 2007
|
#59
|
Remove/check through OLD_BUG_LIST.txt
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Feb 1, 2007
|
#61
|
Make Proof Objects view into standalone RCP application
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Feb 3, 2007
|
#64
|
Decide what to do with ProverStandalone
|
1:pg-eclipse
|
|
|
task
|
alex heneveld
|
new
|
Feb 3, 2007
|
#81
|
Investigate use of Computer Modern Unicode font
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Feb 25, 2007
|
#82
|
Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and isabellesym.sty
|
1:pg-eclipse
|
|
|
task
|
David Aspinall
|
new
|
Feb 25, 2007
|
#195
|
Replace crufty PHP code for interpreting outline mode with some Javascript
|
6:web-and-docs
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 1, 2008
|
#488
|
Display of Ltac debugging mode
|
2:pg-emacs
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 9, 2014
|
#464
|
proof script not displayed after startup
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 19, 2013
|
#465
|
proof script not displayed after startup
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 19, 2013
|
#480
|
[match]es sometimes screw up indentation
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Jul 13, 2013
|
#481
|
proof-set-value does not handle errors in :eval forms of defpacustom
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Jul 17, 2013
|
#483
|
ltac: and constr: should not affect indentation
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Aug 27, 2013
|
#490
|
Bad parsing of .}
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Mar 11, 2014
|
#496
|
Aquamacs point moving
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Sep 6, 2014
|
#497
|
coq auto-compile and spaces in directory names lead to failure
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Oct 4, 2014
|
#499
|
delays between coq messages can cause PG to duplicate some
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Jan 3, 2015
|
#501
|
wrongly embedded pathname in ProofGeneral-4.3pre150202
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 14, 2015
|
#507
|
PG for Coq does not interpret quotes within comments like Coq does
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Aug 29, 2015
|
#508
|
The option -emacs-U is depracated Proof General should use -emacs instead.
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Oct 21, 2015
|
#509
|
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 2, 2016
|
#510
|
coq-time-commands hangs on bullets with Coq-8.5
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Mar 15, 2016
|
#506
|
Please add Proof IDE support to emacs PG
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
new
|
Jun 3, 2015
|
#514
|
Emacs org-mode integration
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
new
|
Aug 1, 2022
|
#457
|
Remove/invoke proof-shell-pre-interrupt-hook
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
new
|
Nov 14, 2012
|
#462
|
Improve library bundling
|
2:pg-emacs
|
|
PG-Emacs-4.4
|
defect
|
David Aspinall
|
new
|
Jan 28, 2013
|
#513
|
Splash screen disappears too quickly
|
2:pg-emacs
|
|
PG-Emacs-4.4
|
defect
|
David Aspinall
|
new
|
May 3, 2016
|
#377
|
Electric-terminator mode next line movement changed
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Oct 11, 2010
|
#429
|
Coq should support *trace* buffer for idtac output
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
reopened
|
Nov 7, 2011
|
#336
|
Toolbar images on Mac Emacsen are super-ugly
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Aug 17, 2010
|