#513 |
Splash screen disappears too quickly
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.4
|
2:pg-emacs
|
#510 |
coq-time-commands hangs on bullets with Coq-8.5
|
new
|
David Aspinall
|
minor
|
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
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#508 |
The option -emacs-U is depracated Proof General should use -emacs instead.
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#507 |
PG for Coq does not interpret quotes within comments like Coq does
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#501 |
wrongly embedded pathname in ProofGeneral-4.3pre150202
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#499 |
delays between coq messages can cause PG to duplicate some
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#498 |
coq-compile-before-require should allow non-source installations
|
new
|
David Aspinall
|
major
|
PG-Emacs-4.3
|
7:prover-coq
|
#497 |
coq auto-compile and spaces in directory names lead to failure
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#496 |
Aquamacs point moving
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#490 |
Bad parsing of .}
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#483 |
ltac: and constr: should not affect indentation
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#481 |
proof-set-value does not handle errors in :eval forms of defpacustom
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#480 |
[match]es sometimes screw up indentation
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#465 |
proof script not displayed after startup
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#464 |
proof script not displayed after startup
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#462 |
Improve library bundling
|
new
|
David Aspinall
|
minor
|
PG-Emacs-4.4
|
2:pg-emacs
|
#456 |
initialization failure with defpacustom :eval
|
new
|
David Aspinall
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#448 |
Repair autotest load sequence so works in compiled and interpreted code
|
accepted
|
David Aspinall
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#401 |
Parser cache does not respect fly-past-comments
|
accepted
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#385 |
Isabelle theorem dependencies display broken
|
accepted
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#377 |
Electric-terminator mode next line movement changed
|
reopened
|
David Aspinall
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#354 |
synchronisation lost with "process rest" and "undo"
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#353 |
"undo last proof command" does not work at the end of theory
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#351 |
Show/hide of proofs in Coq can hide too much
|
accepted
|
David Aspinall
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#336 |
Toolbar images on Mac Emacsen are super-ugly
|
reopened
|
David Aspinall
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#260 |
Path names with spaces are not decoded property on search path
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#256 |
Use prover-specific Preference Initialisers
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#255 |
Refactor concurrency handling for document
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#252 |
Tune script management markers
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#251 |
Exception in editor startup
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#250 |
Interrupt causes document inconsistency
|
assigned
|
David Aspinall
|
blocker
|
|
1:pg-eclipse
|
#247 |
Proof Objects view (IdView) is broken
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#246 |
Fix ProofScriptDocument partitionChangeBroadcast
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#244 |
Comical giant icons in outline view
|
assigned
|
Graham Dutton
|
minor
|
|
1:pg-eclipse
|
#243 |
Parsing errors: whitespace lost in parseresult
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#240 |
Bad behaviour in startup when proof executables (isabelle, isatool) not found
|
assigned
|
Graham Dutton
|
minor
|
|
1:pg-eclipse
|
#194 |
Fix links on web pages and odd mime types for linked files under releases
|
new
|
David Aspinall
|
major
|
|
6:web-and-docs
|
#151 |
Make interface multiple-thread aware
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#150 |
Remove use of PGIP message datatypes
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#149 |
Unify batch and incremental mode of processing
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#148 |
Add "continual validation" mode to PGIP
|
new
|
David Aspinall
|
major
|
|
5:PGIP-design
|
#142 |
New parsescript code in pgip_parser.ML is broken
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#135 |
Quick diff symbol decoding broken
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#127 |
Fix Action Bar active editor switching; simplify actions
|
assigned
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#106 |
Add support for status area message responses
|
new
|
Graham Dutton
|
major
|
|
1:pg-eclipse
|
#105 |
Preference handling refactor: add description text preferences, use those for display, remove ids
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#104 |
Add preference listener to ProofScriptDocument
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#102 |
Simplify message model according to new RNC, change Isabelle to match
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#100 |
Make sure that large volumes of data can be handled by all parts of infrastructure
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#99 |
Reliable interrupts
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#98 |
PGML changes: complete update for PGML 2.0
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#97 |
Add Pretty.markup to parse tree output
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#95 |
Refine spuriouscmd into two: destructivecmd and diagnosticcmd
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#93 |
Propagate position information in errors to make available to interface
|
new
|
David Aspinall
|
major
|
|
4:prover-isabelle
|
#90 |
Folding Improvements
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#89 |
Remove tabs from Isabelle source files (theories, at least)
|
new
|
David Aspinall
|
minor
|
|
4:prover-isabelle
|
#77 |
Partitioning: fix for correct lexical syntax of Isar
|
new
|
Graham Dutton
|
major
|
|
1:pg-eclipse
|
#72 |
Fix prover state indicator
|
new
|
Graham Dutton
|
minor
|
|
1:pg-eclipse
|
#66 |
Make parser more robust and suggest likely causes of error
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#62 |
PGIP console displays messages out-of-order; should allow hiding packets
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#58 |
Hangs during shutdown
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#57 |
Symbol table editor problems: doesn't report correct status, apply is very slow
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#55 |
Parsing whole file is costly; lazy "gathering" parser strategy is flawed
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#54 |
Support file operations save-as, rename, revert properly during script management
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#53 |
Re-implement toolbar button enablers
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#33 |
Fix interrupts: interrupt crashes prover and interrupt ineffective
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#31 |
Decorators not always updated
|
new
|
Graham Dutton
|
minor
|
|
1:pg-eclipse
|
#27 |
Efficiency problems with larger files and larger outputs
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#26 |
Investigate and fix small-scale efficiency problems (e.g. undo in small-ish files)
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#21 |
Refactor to remove DummyDocElement
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#19 |
Use markers/positions for document processed and locked offsets
|
new
|
David Aspinall
|
major
|
|
1:pg-eclipse
|
#14 |
Concurrency fixes
|
new
|
David Aspinall
|
critical
|
|
1:pg-eclipse
|
#12 |
Polish Proof Objects View; Link to Prover Knowledge
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|
#9 |
Fix history in output view
|
new
|
David Aspinall
|
minor
|
|
1:pg-eclipse
|