#498
|
coq-compile-before-require should allow non-source installations
|
7:prover-coq
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Oct 11, 2014
|
#194
|
Fix links on web pages and odd mime types for linked files under releases
|
6:web-and-docs
|
|
|
defect
|
David Aspinall
|
new
|
Feb 1, 2008
|
#195
|
Replace crufty PHP code for interpreting outline mode with some Javascript
|
6:web-and-docs
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 1, 2008
|
#148
|
Add "continual validation" mode to PGIP
|
5:PGIP-design
|
|
|
defect
|
David Aspinall
|
new
|
Sep 16, 2007
|
#101
|
Add scriptreplace and menu choice interaction
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Mar 10, 2007
|
#146
|
Add "sendback" messages to match behaviour added to PG Emacs
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Sep 14, 2007
|
#94
|
Selecting print mode via interface
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Mar 10, 2007
|
#93
|
Propagate position information in errors to make available to interface
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#98
|
PGML changes: complete update for PGML 2.0
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#99
|
Reliable interrupts
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#100
|
Make sure that large volumes of data can be handled by all parts of infrastructure
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#142
|
New parsescript code in pgip_parser.ML is broken
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Sep 14, 2007
|
#149
|
Unify batch and incremental mode of processing
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Sep 16, 2007
|
#151
|
Make interface multiple-thread aware
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Sep 16, 2007
|
#145
|
PGIP parser: add string tokens for categories
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Sep 14, 2007
|
#147
|
Add support for (static) code templates inside Isabelle
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Sep 14, 2007
|
#89
|
Remove tabs from Isabelle source files (theories, at least)
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Feb 28, 2007
|
#95
|
Refine spuriouscmd into two: destructivecmd and diagnosticcmd
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#97
|
Add Pretty.markup to parse tree output
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#102
|
Simplify message model according to new RNC, change Isabelle to match
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Mar 10, 2007
|
#150
|
Remove use of PGIP message datatypes
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Sep 16, 2007
|
#260
|
Path names with spaces are not decoded property on search path
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Nov 27, 2008
|
#96
|
Start/stop quiet: disable these and use statedisplay instead
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Mar 10, 2007
|
#144
|
Build a hybrid top level that removes PG specific one
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Sep 14, 2007
|
#351
|
Show/hide of proofs in Coq can hide too much
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Sep 8, 2010
|
#377
|
Electric-terminator mode next line movement changed
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Oct 11, 2010
|
#448
|
Repair autotest load sequence so works in compiled and interpreted code
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Sep 2, 2012
|
#456
|
initialization failure with defpacustom :eval
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Nov 13, 2012
|
#169
|
Complete buffer history enhancement
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
assigned
|
Dec 13, 2007
|
#273
|
next-error functions: document and streamline
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
accepted
|
Aug 20, 2009
|
#429
|
Coq should support *trace* buffer for idtac output
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
reopened
|
Nov 7, 2011
|
#454
|
coq mode: compile before import fails when no .v file
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
hendrik
|
assigned
|
Oct 2, 2012
|
#276
|
Unicode tokens: resolve font-lock issues, optimise
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Aug 28, 2009
|
#367
|
Fix web pages and update screenshots
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Oct 4, 2010
|
#425
|
Consider simplifying span amalgamation to match prover undo behaviour
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Sep 19, 2011
|
#488
|
Display of Ltac debugging mode
|
2:pg-emacs
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 9, 2014
|
#336
|
Toolbar images on Mac Emacsen are super-ugly
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Aug 17, 2010
|
#385
|
Isabelle theorem dependencies display broken
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Jan 23, 2011
|
#401
|
Parser cache does not respect fly-past-comments
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
May 16, 2011
|
#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
|
#208
|
Generalise Coq's modeline subgoal counter for other provers
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
accepted
|
Jun 13, 2008
|
#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
|
#361
|
Generic adjustment of prover's pretty-printing width
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Oct 1, 2010
|
#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
|
#364
|
Unify proof-query-identifier and pg-identifier-near-point-query (cleanup)
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Oct 1, 2010
|
#250
|
Interrupt causes document inconsistency
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
assigned
|
Sep 5, 2008
|
#249
|
Script management error for locales; undo action failure should not generate markers
|
1:pg-eclipse
|
|
|
|
David Aspinall
|
assigned
|
Sep 4, 2008
|
#14
|
Concurrency fixes
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#66
|
Make parser more robust and suggest likely causes of error
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Feb 3, 2007
|
#246
|
Fix ProofScriptDocument partitionChangeBroadcast
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 4, 2008
|
#251
|
Exception in editor startup
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 6, 2008
|
#252
|
Tune script management markers
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 8, 2008
|
#255
|
Refactor concurrency handling for document
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 15, 2008
|
#38
|
Add automated testing framework
|
1:pg-eclipse
|
|
|
enhancement
|
alex heneveld
|
new
|
Jan 30, 2007
|
#42
|
Extract Isabelle-specific behaviour; design prover extension point
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#19
|
Use markers/positions for document processed and locked offsets
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#21
|
Refactor to remove DummyDocElement
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#26
|
Investigate and fix small-scale efficiency problems (e.g. undo in small-ish files)
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#27
|
Efficiency problems with larger files and larger outputs
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#33
|
Fix interrupts: interrupt crashes prover and interrupt ineffective
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jan 30, 2007
|
#54
|
Support file operations save-as, rename, revert properly during script management
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Feb 1, 2007
|
#55
|
Parsing whole file is costly; lazy "gathering" parser strategy is flawed
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Feb 1, 2007
|
#77
|
Partitioning: fix for correct lexical syntax of Isar
|
1:pg-eclipse
|
|
|
defect
|
Graham Dutton
|
new
|
Feb 23, 2007
|
#90
|
Folding Improvements
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Feb 28, 2007
|
#106
|
Add support for status area message responses
|
1:pg-eclipse
|
|
|
defect
|
Graham Dutton
|
new
|
Mar 18, 2007
|
#127
|
Fix Action Bar active editor switching; simplify actions
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
assigned
|
Jul 7, 2007
|
#135
|
Quick diff symbol decoding broken
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Jul 19, 2007
|
#243
|
Parsing errors: whitespace lost in parseresult
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Aug 31, 2008
|
#247
|
Proof Objects view (IdView) is broken
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 4, 2008
|
#353
|
"undo last proof command" does not work at the end of theory
|
1:pg-eclipse
|
|
|
defect
|
David Aspinall
|
new
|
Sep 14, 2010
|
#5
|
Replace ThreadPool with Eclipse job management
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 29, 2007
|
#10
|
Refactor and enhance document model
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 29, 2007
|
#35
|
Implement Java PGIP abstraction, independently of Eclipse code
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#37
|
ProverKnowledge updates and improvements
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#40
|
Implement document regions and annotations/markers for colouring
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#41
|
Revive GEF dependency graph viewer as a separate plugin
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#44
|
Support openblock/closeblock elements in prover parse output.
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#45
|
Use workbench progress feedbacks; provide busy indications
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 30, 2007
|
#47
|
Complete configuration of <lexicalsyntax> elements
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
assigned
|
Jan 30, 2007
|
#73
|
Enhancements for Proof Objects view
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 17, 2007
|
#75
|
Proof Script Editor context menu improvements
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 21, 2007
|
#76
|
Add Prove-As-You-Type option
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 21, 2007
|
#79
|
Improve symbols: support table inclusions; add Mac and Windows overrides
|
1:pg-eclipse
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 25, 2007
|
#87
|
Add support for indentation in proof script editor
|
1:pg-eclipse
|
|
|
enhancement
|
Graham Dutton
|
new
|
Feb 27, 2007
|