id Summary Status Owner Type Milestone Priority 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 17 Add clear button for prover output accepted 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 158 cursor positioning is wrong when sending commands accepted Graham Dutton enhancement minor 195 Replace crufty PHP code for interpreting outline mode with some Javascript new David Aspinall enhancement minor 208 Generalise Coq's modeline subgoal counter for other provers accepted David Aspinall enhancement PG-Emacs-4.3 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 PG-Emacs-4.3 minor 354 "synchronisation lost with ""process rest"" and ""undo""" new David Aspinall defect minor 361 Generic adjustment of prover's pretty-printing width accepted David Aspinall task PG-Emacs-4.3 minor 385 Isabelle theorem dependencies display broken accepted David Aspinall defect PG-Emacs-4.3 minor 401 Parser cache does not respect fly-past-comments accepted David Aspinall defect PG-Emacs-4.3 minor 457 Remove/invoke proof-shell-pre-interrupt-hook new David Aspinall task PG-Emacs-4.3 minor 462 Improve library bundling new David Aspinall defect PG-Emacs-4.4 minor 464 proof script not displayed after startup new David Aspinall defect PG-Emacs-4.3 minor 465 proof script not displayed after startup new David Aspinall defect PG-Emacs-4.3 minor 480 [match]es sometimes screw up indentation new David Aspinall defect PG-Emacs-4.3 minor 481 proof-set-value does not handle errors in :eval forms of defpacustom new David Aspinall defect PG-Emacs-4.3 minor 483 ltac: and constr: should not affect indentation new David Aspinall defect PG-Emacs-4.3 minor 488 Display of Ltac debugging mode new David Aspinall enhancement minor 490 Bad parsing of .} new David Aspinall defect PG-Emacs-4.3 minor 496 Aquamacs point moving new David Aspinall defect PG-Emacs-4.3 minor 497 coq auto-compile and spaces in directory names lead to failure new David Aspinall defect PG-Emacs-4.3 minor 499 delays between coq messages can cause PG to duplicate some new David Aspinall defect PG-Emacs-4.3 minor 501 wrongly embedded pathname in ProofGeneral-4.3pre150202 new David Aspinall defect PG-Emacs-4.3 minor 506 Please add Proof IDE support to emacs PG new David Aspinall enhancement PG-Emacs-4.3 minor 507 PG for Coq does not interpret quotes within comments like Coq does new David Aspinall defect PG-Emacs-4.3 minor 508 The option -emacs-U is depracated Proof General should use -emacs instead. new David Aspinall defect PG-Emacs-4.3 minor 509 isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined. new David Aspinall defect PG-Emacs-4.3 minor 510 coq-time-commands hangs on bullets with Coq-8.5 new David Aspinall defect PG-Emacs-4.3 minor 513 Splash screen disappears too quickly new David Aspinall defect PG-Emacs-4.4 minor 514 Emacs org-mode integration new David Aspinall enhancement PG-Emacs-4.3 minor