id Summary Status Owner Type Priority Milestone 250 Interrupt causes document inconsistency assigned David Aspinall defect blocker 14 Concurrency fixes new David Aspinall defect critical 38 Add automated testing framework new alex heneveld enhancement critical 42 Extract Isabelle-specific behaviour; design prover extension point new David Aspinall enhancement critical 66 Make parser more robust and suggest likely causes of error new David Aspinall defect critical 246 Fix ProofScriptDocument partitionChangeBroadcast new David Aspinall defect critical 249 Script management error for locales; undo action failure should not generate markers assigned David Aspinall critical 251 Exception in editor startup new David Aspinall defect critical 252 Tune script management markers new David Aspinall defect critical 255 Refactor concurrency handling for document new David Aspinall defect critical 3 Improve code quality: address J2SE best practices in TPTP analysis new somebody task major 5 Replace ThreadPool with Eclipse job management new David Aspinall enhancement major 10 Refactor and enhance document model new David Aspinall enhancement major 19 Use markers/positions for document processed and locked offsets new David Aspinall defect major 21 Refactor to remove DummyDocElement new David Aspinall defect major 26 Investigate and fix small-scale efficiency problems (e.g. undo in small-ish files) new David Aspinall defect major 27 Efficiency problems with larger files and larger outputs new David Aspinall defect major 33 Fix interrupts: interrupt crashes prover and interrupt ineffective new David Aspinall defect major 34 Event processing cleanups assigned David Aspinall task major 35 Implement Java PGIP abstraction, independently of Eclipse code new David Aspinall enhancement major 37 ProverKnowledge updates and improvements new David Aspinall enhancement major 40 Implement document regions and annotations/markers for colouring new David Aspinall enhancement major 41 Revive GEF dependency graph viewer as a separate plugin new David Aspinall enhancement major 44 Support openblock/closeblock elements in prover parse output. new David Aspinall enhancement major 45 Use workbench progress feedbacks; provide busy indications new David Aspinall enhancement major 47 Complete configuration of elements assigned David Aspinall enhancement major 54 Support file operations save-as, rename, revert properly during script management new David Aspinall defect major 55 "Parsing whole file is costly; lazy ""gathering"" parser strategy is flawed" new David Aspinall defect major 65 Use FindBugs to detect possible bugs new David Aspinall task major 73 Enhancements for Proof Objects view new David Aspinall enhancement major 75 Proof Script Editor context menu improvements new David Aspinall enhancement major 76 Add Prove-As-You-Type option new David Aspinall enhancement major 77 Partitioning: fix for correct lexical syntax of Isar new Graham Dutton defect major 79 Improve symbols: support table inclusions; add Mac and Windows overrides new David Aspinall enhancement major 87 Add support for indentation in proof script editor new Graham Dutton enhancement major 90 Folding Improvements new David Aspinall defect major 93 Propagate position information in errors to make available to interface new David Aspinall defect major 98 PGML changes: complete update for PGML 2.0 new David Aspinall defect major 99 Reliable interrupts new David Aspinall defect major 100 Make sure that large volumes of data can be handled by all parts of infrastructure new David Aspinall defect major 101 Add scriptreplace and menu choice interaction new David Aspinall enhancement major 106 Add support for status area message responses new Graham Dutton defect major 108 Support proof object searching via search dialog new David Aspinall enhancement major 122 Use Batch Build Command and Project Batch Build Command new David Aspinall enhancement major 125 Use message to configure prover-specific preferences new Graham Dutton enhancement major 127 Fix Action Bar active editor switching; simplify actions assigned David Aspinall defect major 132 Packaging for 1.0.6/3.4 releases new Graham Dutton task major 134 Generalise lexing to better match Isar syntax assigned David Aspinall enhancement major 135 Quick diff symbol decoding broken new David Aspinall defect major 136 Add compare support for proof scripts new David Aspinall enhancement major 142 New parsescript code in pgip_parser.ML is broken new David Aspinall defect major 145 PGIP parser: add string tokens for categories new David Aspinall enhancement major 146 "Add ""sendback"" messages to match behaviour added to PG Emacs" new David Aspinall enhancement major 147 Add support for (static) code templates inside Isabelle new David Aspinall enhancement major 148 "Add ""continual validation"" mode to PGIP" new David Aspinall defect major 149 Unify batch and incremental mode of processing new David Aspinall defect major 151 Make interface multiple-thread aware new David Aspinall defect major 169 Complete buffer history enhancement assigned David Aspinall enhancement major PG-Emacs-4.3 194 Fix links on web pages and odd mime types for linked files under releases new David Aspinall defect major 243 Parsing errors: whitespace lost in parseresult new David Aspinall defect major 247 Proof Objects view (IdView) is broken new David Aspinall defect major 353 """undo last proof command"" does not work at the end of theory" new David Aspinall defect major 377 Electric-terminator mode next line movement changed reopened David Aspinall defect major PG-Emacs-4.3 429 Coq should support *trace* buffer for idtac output reopened David Aspinall enhancement major PG-Emacs-4.3 454 coq mode: compile before import fails when no .v file assigned hendrik enhancement major PG-Emacs-4.3 456 initialization failure with defpacustom :eval new David Aspinall defect major PG-Emacs-4.3 498 coq-compile-before-require should allow non-source installations new David Aspinall defect major PG-Emacs-4.3 9 Fix history in output view new David Aspinall defect minor 11 Builder for parsing/proving files automatically new David Aspinall enhancement minor 12 Polish Proof Objects View; Link to Prover Knowledge new David Aspinall defect minor 13 Add proof object search facilities to IdView assigned Graham Dutton enhancement minor 18 Add hover for prover output (on any blue space) new David Aspinall enhancement minor 22 Refactor SessionManager assigned David Aspinall enhancement minor 23 Test and refine capabilities/activities new Graham Dutton enhancement minor 25 Review in-code TODO and FIXME tasks new David Aspinall task minor 29 Symbol table editing scheme: fix filename and add edit action rather than create new David Aspinall enhancement minor 31 Decorators not always updated new Graham Dutton defect minor 32 Add some user documentation new David Aspinall enhancement minor 39 Code cleanups: use tag CLEANUP for old code prior to removal new David Aspinall task minor 43 Improve output markup (pgml.xsl) assigned Graham Dutton enhancement minor 46 Extra view for Problem Details new David Aspinall enhancement minor 51 Add processing direction to 'active script' decorator new anonymous enhancement minor 53 Re-implement toolbar button enablers new David Aspinall defect minor 57 Symbol table editor problems: doesn't report correct status, apply is very slow new David Aspinall defect minor 58 Hangs during shutdown new David Aspinall defect minor 59 Remove/check through OLD_BUG_LIST.txt new David Aspinall task minor 60 Improve icons throughout new David Aspinall enhancement minor 61 Make Proof Objects view into standalone RCP application new David Aspinall task minor 62 PGIP console displays messages out-of-order; should allow hiding packets new David Aspinall defect minor 64 Decide what to do with ProverStandalone new alex heneveld task minor 72 Fix prover state indicator new Graham Dutton defect minor 80 Improve symbols/character display: allow superscript, subscript (and maybe bold, italic, colours, ...) new David Aspinall enhancement minor 81 Investigate use of Computer Modern Unicode font new David Aspinall task minor 82 Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and isabellesym.sty new David Aspinall task minor 85 Outline view improvements new David Aspinall enhancement minor 89 Remove tabs from Isabelle source files (theories, at least) new David Aspinall defect minor 94 Selecting print mode via interface new David Aspinall enhancement minor 95 Refine spuriouscmd into two: destructivecmd and diagnosticcmd new David Aspinall defect minor 96 Start/stop quiet: disable these and use statedisplay instead new David Aspinall enhancement minor 97 Add Pretty.markup to parse tree output new David Aspinall defect minor 102 Simplify message model according to new RNC, change Isabelle to match new David Aspinall defect minor 104 Add preference listener to ProofScriptDocument new David Aspinall defect minor 105 Preference handling refactor: add description text preferences, use those for display, remove ids new David Aspinall defect minor 107 Support text file searching with symbol encoding/decoding new Graham Dutton enhancement minor 130 Add project batch builder new Graham Dutton enhancement minor 133 Enhance proof project nature: add proof project preference, use prover-specifics new David Aspinall enhancement minor 144 Build a hybrid top level that removes PG specific one new David Aspinall enhancement minor 150 Remove use of PGIP message datatypes new David Aspinall defect minor 195 Replace crufty PHP code for interpreting outline mode with some Javascript new David Aspinall enhancement minor 239 Remove reliance on dom4j new David Aspinall enhancement minor 240 Bad behaviour in startup when proof executables (isabelle, isatool) not found assigned Graham Dutton defect minor 244 Comical giant icons in outline view assigned Graham Dutton defect minor 256 Use prover-specific Preference Initialisers new David Aspinall defect minor 260 Path names with spaces are not decoded property on search path new David Aspinall defect minor 336 Toolbar images on Mac Emacsen are super-ugly reopened David Aspinall defect minor PG-Emacs-4.3 354 "synchronisation lost with ""process rest"" and ""undo""" new David Aspinall defect minor 457 Remove/invoke proof-shell-pre-interrupt-hook new David Aspinall task minor PG-Emacs-4.3 462 Improve library bundling new David Aspinall defect minor PG-Emacs-4.4 464 proof script not displayed after startup new David Aspinall defect minor PG-Emacs-4.3 465 proof script not displayed after startup new David Aspinall defect minor PG-Emacs-4.3 480 [match]es sometimes screw up indentation new David Aspinall defect minor PG-Emacs-4.3 481 proof-set-value does not handle errors in :eval forms of defpacustom new David Aspinall defect minor PG-Emacs-4.3 483 ltac: and constr: should not affect indentation new David Aspinall defect minor PG-Emacs-4.3 488 Display of Ltac debugging mode new David Aspinall enhancement minor 490 Bad parsing of .} new David Aspinall defect minor PG-Emacs-4.3 496 Aquamacs point moving new David Aspinall defect minor PG-Emacs-4.3 497 coq auto-compile and spaces in directory names lead to failure new David Aspinall defect minor PG-Emacs-4.3 499 delays between coq messages can cause PG to duplicate some new David Aspinall defect minor PG-Emacs-4.3 501 wrongly embedded pathname in ProofGeneral-4.3pre150202 new David Aspinall defect minor PG-Emacs-4.3 506 Please add Proof IDE support to emacs PG new David Aspinall enhancement minor PG-Emacs-4.3 507 PG for Coq does not interpret quotes within comments like Coq does new David Aspinall defect minor PG-Emacs-4.3 508 The option -emacs-U is depracated Proof General should use -emacs instead. new David Aspinall defect minor PG-Emacs-4.3 509 isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined. new David Aspinall defect minor PG-Emacs-4.3 510 coq-time-commands hangs on bullets with Coq-8.5 new David Aspinall defect minor PG-Emacs-4.3 513 Splash screen disappears too quickly new David Aspinall defect minor PG-Emacs-4.4 514 Emacs org-mode integration new David Aspinall enhancement minor PG-Emacs-4.3