#462
|
Improve library bundling
|
2:pg-emacs
|
|
PG-Emacs-4.4
|
defect
|
David Aspinall
|
new
|
Mar 13, 2015
|
#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
|
#377
|
Electric-terminator mode next line movement changed
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Jun 22, 2014
|
#490
|
Bad parsing of .}
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Mar 11, 2014
|
#488
|
Display of Ltac debugging mode
|
2:pg-emacs
|
|
|
enhancement
|
David Aspinall
|
new
|
Jan 9, 2014
|
#483
|
ltac: and constr: should not affect indentation
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Aug 27, 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
|
#480
|
[match]es sometimes screw up indentation
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Jul 13, 2013
|
#454
|
coq mode: compile before import fails when no .v file
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
hendrik
|
assigned
|
Jul 4, 2013
|
#456
|
initialization failure with defpacustom :eval
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Jul 4, 2013
|
#465
|
proof script not displayed after startup
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 19, 2013
|
#464
|
proof script not displayed after startup
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
Feb 19, 2013
|
#457
|
Remove/invoke proof-shell-pre-interrupt-hook
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
new
|
Nov 14, 2012
|
#208
|
Generalise Coq's modeline subgoal counter for other provers
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
accepted
|
Sep 25, 2012
|
#273
|
next-error functions: document and streamline
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
accepted
|
Sep 25, 2012
|
#448
|
Repair autotest load sequence so works in compiled and interpreted code
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Sep 14, 2012
|
#401
|
Parser cache does not respect fly-past-comments
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Aug 14, 2012
|
#336
|
Toolbar images on Mac Emacsen are super-ugly
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
reopened
|
Aug 14, 2012
|
#385
|
Isabelle theorem dependencies display broken
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Aug 14, 2012
|
#351
|
Show/hide of proofs in Coq can hide too much
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
accepted
|
Aug 9, 2012
|
#367
|
Fix web pages and update screenshots
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Aug 9, 2012
|
#425
|
Consider simplifying span amalgamation to match prover undo behaviour
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Apr 18, 2012
|
#364
|
Unify proof-query-identifier and pg-identifier-near-point-query (cleanup)
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Apr 18, 2012
|
#361
|
Generic adjustment of prover's pretty-printing width
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
task
|
David Aspinall
|
accepted
|
Apr 18, 2012
|
#169
|
Complete buffer history enhancement
|
2:pg-emacs
|
|
PG-Emacs-4.3
|
enhancement
|
David Aspinall
|
assigned
|
Apr 18, 2012
|
#149
|
Unify batch and incremental mode of processing
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#151
|
Make interface multiple-thread aware
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#89
|
Remove tabs from Isabelle source files (theories, at least)
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#95
|
Refine spuriouscmd into two: destructivecmd and diagnosticcmd
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#96
|
Start/stop quiet: disable these and use statedisplay instead
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#97
|
Add Pretty.markup to parse tree output
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#99
|
Reliable interrupts
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#100
|
Make sure that large volumes of data can be handled by all parts of infrastructure
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#150
|
Remove use of PGIP message datatypes
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#260
|
Path names with spaces are not decoded property on search path
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#93
|
Propagate position information in errors to make available to interface
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#98
|
PGML changes: complete update for PGML 2.0
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#102
|
Simplify message model according to new RNC, change Isabelle to match
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#142
|
New parsescript code in pgip_parser.ML is broken
|
4:prover-isabelle
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#144
|
Build a hybrid top level that removes PG specific one
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#145
|
PGIP parser: add string tokens for categories
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#147
|
Add support for (static) code templates inside Isabelle
|
4:prover-isabelle
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#148
|
Add "continual validation" mode to PGIP
|
5:PGIP-design
|
|
|
defect
|
David Aspinall
|
new
|
Apr 16, 2013
|
#94
|
Selecting print mode via interface
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#101
|
Add scriptreplace and menu choice interaction
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#146
|
Add "sendback" messages to match behaviour added to PG Emacs
|
5:PGIP-design
|
|
|
enhancement
|
David Aspinall
|
new
|
Apr 16, 2013
|
#195
|
Replace crufty PHP code for interpreting outline mode with some Javascript
|
6:web-and-docs
|
|
|
enhancement
|
David Aspinall
|
new
|
Feb 22, 2010
|
#194
|
Fix links on web pages and odd mime types for linked files under releases
|
6:web-and-docs
|
|
|
defect
|
David Aspinall
|
new
|
Feb 22, 2010
|
#498
|
coq-compile-before-require should allow non-source installations
|
7:prover-coq
|
|
PG-Emacs-4.3
|
defect
|
David Aspinall
|
new
|
May 7, 2015
|