#19 |
Use markers/positions for document processed and locked offsets
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#21 |
Refactor to remove DummyDocElement
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#26 |
Investigate and fix small-scale efficiency problems (e.g. undo in small-ish files)
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#27 |
Efficiency problems with larger files and larger outputs
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#33 |
Fix interrupts: interrupt crashes prover and interrupt ineffective
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#54 |
Support file operations save-as, rename, revert properly during script management
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#55 |
Parsing whole file is costly; lazy "gathering" parser strategy is flawed
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#77 |
Partitioning: fix for correct lexical syntax of Isar
|
new
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#90 |
Folding Improvements
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#93 |
Propagate position information in errors to make available to interface
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#98 |
PGML changes: complete update for PGML 2.0
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#99 |
Reliable interrupts
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#100 |
Make sure that large volumes of data can be handled by all parts of infrastructure
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#106 |
Add support for status area message responses
|
new
|
Graham Dutton
|
defect
|
|
1:pg-eclipse
|
#127 |
Fix Action Bar active editor switching; simplify actions
|
assigned
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#135 |
Quick diff symbol decoding broken
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#142 |
New parsescript code in pgip_parser.ML is broken
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#148 |
Add "continual validation" mode to PGIP
|
new
|
David Aspinall
|
defect
|
|
5:PGIP-design
|
#149 |
Unify batch and incremental mode of processing
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#151 |
Make interface multiple-thread aware
|
new
|
David Aspinall
|
defect
|
|
4:prover-isabelle
|
#194 |
Fix links on web pages and odd mime types for linked files under releases
|
new
|
David Aspinall
|
defect
|
|
6:web-and-docs
|
#243 |
Parsing errors: whitespace lost in parseresult
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#247 |
Proof Objects view (IdView) is broken
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#351 |
Show/hide of proofs in Coq can hide too much
|
accepted
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#353 |
"undo last proof command" does not work at the end of theory
|
new
|
David Aspinall
|
defect
|
|
1:pg-eclipse
|
#377 |
Electric-terminator mode next line movement changed
|
reopened
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#448 |
Repair autotest load sequence so works in compiled and interpreted code
|
accepted
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#456 |
initialization failure with defpacustom :eval
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
2:pg-emacs
|
#498 |
coq-compile-before-require should allow non-source installations
|
new
|
David Aspinall
|
defect
|
PG-Emacs-4.3
|
7:prover-coq
|
#5 |
Replace ThreadPool with Eclipse job management
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#10 |
Refactor and enhance document model
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#35 |
Implement Java PGIP abstraction, independently of Eclipse code
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#37 |
ProverKnowledge updates and improvements
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#40 |
Implement document regions and annotations/markers for colouring
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#41 |
Revive GEF dependency graph viewer as a separate plugin
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#44 |
Support openblock/closeblock elements in prover parse output.
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#45 |
Use workbench progress feedbacks; provide busy indications
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#47 |
Complete configuration of <lexicalsyntax> elements
|
assigned
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#73 |
Enhancements for Proof Objects view
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#75 |
Proof Script Editor context menu improvements
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#76 |
Add Prove-As-You-Type option
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#79 |
Improve symbols: support table inclusions; add Mac and Windows overrides
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#87 |
Add support for indentation in proof script editor
|
new
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#101 |
Add scriptreplace and menu choice interaction
|
new
|
David Aspinall
|
enhancement
|
|
5:PGIP-design
|
#108 |
Support proof object searching via search dialog
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#122 |
Use Batch Build Command and Project Batch Build Command
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#125 |
Use <askprefs> message to configure prover-specific preferences
|
new
|
Graham Dutton
|
enhancement
|
|
1:pg-eclipse
|
#134 |
Generalise lexing to better match Isar syntax
|
assigned
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#136 |
Add compare support for proof scripts
|
new
|
David Aspinall
|
enhancement
|
|
1:pg-eclipse
|
#145 |
PGIP parser: add string tokens for categories
|
new
|
David Aspinall
|
enhancement
|
|
4:prover-isabelle
|
#146 |
Add "sendback" messages to match behaviour added to PG Emacs
|
new
|
David Aspinall
|
enhancement
|
|
5:PGIP-design
|
#147 |
Add support for (static) code templates inside Isabelle
|
new
|
David Aspinall
|
enhancement
|
|
4:prover-isabelle
|
#169 |
Complete buffer history enhancement
|
assigned
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#273 |
next-error functions: document and streamline
|
accepted
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#429 |
Coq should support *trace* buffer for idtac output
|
reopened
|
David Aspinall
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#454 |
coq mode: compile before import fails when no .v file
|
assigned
|
hendrik
|
enhancement
|
PG-Emacs-4.3
|
2:pg-emacs
|
#3 |
Improve code quality: address J2SE best practices in TPTP analysis
|
new
|
somebody
|
task
|
|
1:pg-eclipse
|
#34 |
Event processing cleanups
|
assigned
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#65 |
Use FindBugs to detect possible bugs
|
new
|
David Aspinall
|
task
|
|
1:pg-eclipse
|
#132 |
Packaging for 1.0.6/3.4 releases
|
new
|
Graham Dutton
|
task
|
|
1:pg-eclipse
|
#276 |
Unicode tokens: resolve font-lock issues, optimise
|
accepted
|
David Aspinall
|
task
|
PG-Emacs-4.3
|
2:pg-emacs
|
#367 |
Fix web pages and update screenshots
|
accepted
|
David Aspinall
|
task
|
PG-Emacs-4.3
|
2:pg-emacs
|
#425 |
Consider simplifying span amalgamation to match prover undo behaviour
|
accepted
|
David Aspinall
|
task
|
PG-Emacs-4.3
|
2:pg-emacs
|