Timeline
Apr 16, 2007:
- 1:29 PM Ticket #109 (Missing output from Coq) closed by
- fixed: OK, this should be fixed. When Coq outputs a message followed by the …
Apr 5, 2007:
- 6:20 PM Ticket #112 (Filter out control characters in shell buffer or copy from shell buffer) created by
- Any idea how I can get rid of the characters such as Ú that appear in …
Mar 23, 2007:
- 1:24 PM Ticket #111 (Centering the goal window on the right part of the goals) created by
- In coq, when doing large proofs, the goals window tends to not be …
- 9:28 AM Ticket #110 (Search Rewrite and Search About queries for Proof General/Coq) created by
- The options "Search Rewrite ..." and "Search About ..." do not work in …
Mar 19, 2007:
- 10:14 AM WikiStart edited by
- (diff)
- 10:06 AM Ticket #109 (Missing output from Coq) created by
- Dear Proof General developers, In Coq, the identity tactic, idtac, is …
Mar 18, 2007:
- 12:15 PM Ticket #108 (Support proof object searching via search dialog) created by
- As a supplement to the IdView?, we may support proof object searching …
- 12:13 PM Ticket #107 (Support text file searching with symbol encoding/decoding) created by
- Text file search should support symbol decoding (tokenisation) in …
- 12:05 PM Ticket #8 (Cleanup active script handling in actions) closed by
- fixed: This is pretty much fixed now, although further refactoring of …
- 12:04 PM Ticket #106 (Add support for status area message responses) created by
- PGIP normalresponses with the area set to be "status" should be …
- 11:36 AM Ticket #6 (Add code folding for proof scripts) closed by
- fixed: Good basic support for code folding has now been added. It is enabled …
Mar 17, 2007:
- 4:33 PM Ticket #105 (Preference handling refactor: add description text preferences, use ...) created by
- Preference files use name attribute both for lookup of preferences and …
- 11:52 AM Ticket #104 (Add preference listener to ProofScriptDocument) created by
- This can usefully monitor several kinds of preference changes, e.g. …
- 11:50 AM Ticket #103 (Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)) closed by
- fixed: This has actually been provided a while ago, as coq-utf-safe.
Mar 12, 2007:
- 10:27 PM Ticket #103 (Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)) created by
- Coq still uses the troublesome UTF-8 prefix character that causes the …
Mar 10, 2007:
- 6:32 PM Ticket #102 (Simplify message model according to new RNC, change Isabelle to match) created by
- Some further discussion maybe required, but proposal in draft RNC for …
- 6:32 PM Ticket #101 (Add scriptreplace and menu choice interaction) created by
- * We have messages for (statically) configuring prover operations and …
- 4:59 PM Ticket #100 (Make sure that large volumes of data can be handled by all parts of ...) created by
- This is the old problem of too much output "choking" * In some …
- 4:53 PM Ticket #99 (Reliable interrupts) created by
- 4:49 PM Ticket #84 (Remove double-quoted XML output from term display) closed by
- fixed
- 4:48 PM Ticket #98 (PGML changes: complete update for PGML 2.0) created by
- This will come from * tokenised input (theory presentation) * …
- 4:02 PM Ticket #97 (Add Pretty.markup to parse tree output) created by
- This will allow several things: * Markup on constants as well as …
- 3:25 PM Ticket #96 (Start/stop quiet: disable these and use statedisplay instead) created by
- Small change in
proof_general_pgip.ML: disable printing by default, … - 3:24 PM Ticket #95 (Refine spuriouscmd into two: destructivecmd and diagnosticcmd) created by
- Makarius notes that spuriouscmd cannot be pruned from scripts because …
- 2:43 PM Ticket #94 (Selecting print mode via interface) created by
- Should we have some way of automatically configuring the output …
- 9:30 AM Ticket #93 (Propagate position information in errors to make available to interface) created by
- Some exceptions in Isabelle already carry position information. …
- 9:27 AM Ticket #92 (Attempt recovery from XML parse errors in PGIP main loop) created by
- Isabelle exits in case of erroneous XML input. It could be made more …
Mar 2, 2007:
- 11:38 PM Ticket #91 (PGML: add markup for subscript, superscript, bold, ...) created by
- PGML does not have this markup. Subscript and superscript, at least, …
Feb 28, 2007:
- 1:52 PM Ticket #90 (Folding Improvements) created by
- Some desirable folding improvements are: 1. Check heuristic for …
- 1:40 PM Ticket #89 (Remove tabs from Isabelle source files (theories, at least)) created by
- The default tab width in Emacs is 8, in Eclipse it is 4. This messes …
Feb 27, 2007:
- 9:05 PM Ticket #88 (Buffer invisibility spec bug with Emacs 22) created by
- [Reported by Michaël Cadilhac] I'm an Emacs22 user of Proof General, …
- 8:32 PM Ticket #87 (Add support for indentation in proof script editor) created by
- Indentation can be controlled by either or both of: * …
- 1:39 PM Ticket #86 (Fix parse edit offset) created by
- Editing document sets the parse edit offset, the position from which …
- 1:37 PM Ticket #85 (Outline view improvements) created by
- Some possible enhancements to the outline view: 1. fix hiding of …
- 1:13 PM Ticket #78 (Preferences: support dynamically computed defaults) closed by
- fixed: I've now added a simpler mechanism for allowing OS-specific preference …
- 12:54 PM Ticket #36 (Split stream for console into input/output and give input a different ...) closed by
- fixed: Above comment seems inaccurate:
org.eclipse.ui.console.IOConsole… - 10:30 AM Ticket #84 (Remove double-quoted XML output from term display) created by
- The current Isabelle CVS version displays goals correctly but …
Feb 25, 2007:
- 1:49 PM Ticket #83 (Fix script parsing to produce reliable and speedy <parseresult> outputs) created by
- See Pure/ProofGeneral?/parsing.ML. This is an absolutely essential …
- 1:12 PM Ticket #82 (Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and ...) created by
- * Isabelle.sym should be a superset of x-symbol-isabelle.el and …
- 1:03 PM Ticket #81 (Investigate use of Computer Modern Unicode font) created by
- Computer Modern Unicode may give a more uniform (across platforms) …
- 12:56 PM Ticket #80 (Improve symbols/character display: allow superscript, subscript (and ...) created by
- X-Symbol in Proof General Emacs allows superscripting and subscripting …
- 12:34 PM Ticket #79 (Improve symbols: support table inclusions; add Mac and Windows overrides) created by
- Present Isabelle.sym file works well on Linux/Fedora? Core 6. We …
- 12:32 PM Ticket #78 (Preferences: support dynamically computed defaults) created by
- The preference mechanism should support dynamically computed defaults. …
Feb 24, 2007:
Feb 23, 2007:
- 1:14 PM Ticket #77 (Partitioning: fix for correct lexical syntax of Isar) created by
- Lexical syntax fixes required. We can fix these first in main Java …
Feb 22, 2007:
Feb 21, 2007:
- 12:54 PM Ticket #76 (Add Prove-As-You-Type option) created by
- This is an idea for an updated version of the "electric terminator" …
- 11:46 AM Ticket #75 (Proof Script Editor context menu improvements) created by
- The context menu (right-click) in the proof script editor needs some …
Feb 19, 2007:
- 1:55 PM AboutTrac created by
- 1:32 PM Ticket #74 (Coq: bug in electric terminator: typing '.' in comment causes comment ...) created by
- When I type a '.' within a comment, the comment is sent to Coq and …
Feb 17, 2007:
- 5:54 PM Ticket #63 (Improve symbols: fill out default table, add ascii-symbol completion) closed by
- fixed: Both of these added now. New Isabelle symbol table is: …
- 12:48 PM Ticket #73 (Enhancements for Proof Objects view) created by
- Some possible improvements to the Proof Objects view are: * Make …
Feb 7, 2007:
- 5:05 PM Ticket #72 (Fix prover state indicator) created by
- Currently a partially-implement prover state indicator in the …
- 2:26 PM Ticket #71 (Add Error Decoration to documents; optimise Active Script Decoration) created by
- Decoration which annotates the current error/warning state is …
Feb 5, 2007:
- 1:16 PM Ticket #70 (Add documentation for developer-recommended plugins) created by
- Suggested so far (ones I use): * TPTP (profiling and static …
Feb 4, 2007:
- 3:14 PM Ticket #69 (PGMarkerMethods: skip spaces in document before error marker start) created by
- If error marker has been set by us based on command from document, …
- 2:25 PM Ticket #68 (Move to Eclipse 3.3 at 3.3M5) created by
- 3.3M5 stable is due 9th February. We should migrate code and …
- 1:23 PM Ticket #67 (Move to Java 6...) created by
- This ticket is for notes on moving to Java 6. * Points in code to …
Feb 3, 2007:
- 4:00 PM Ticket #66 (Make parser more robust and suggest likely causes of error) created by
- The parser reports problems reconciling parseresult with the input …
- 2:15 PM Ticket #65 (Use FindBugs to detect possible bugs) created by
- All developers are recommended to use FindBugs to help detect …
- 1:53 PM Ticket #64 (Decide what to do with ProverStandalone) created by
- Should this code be retained or discarded? Not clear how it fits into …
- 12:44 PM Ticket #63 (Improve symbols: fill out default table, add ascii-symbol completion) created by
- * The default symbol table should have a more complete set of …
- 11:31 AM Ticket #62 (PGIP console displays messages out-of-order; should allow hiding packets) created by
- Sometimes responses are shown in the console before the commands that …
- 9:56 AM Ticket #61 (Make Proof Objects view into standalone RCP application) created by
- The Proof Objects view (in IdView.java) is nice for browsing objects …
Feb 1, 2007:
- 10:12 PM Ticket #60 (Improve icons throughout) created by
- We need more icons and improved existing ones. Generally icons should …
- 10:02 PM Ticket #59 (Remove/check through OLD_BUG_LIST.txt) created by
- Most of the old bugs reported before Sep 2006 are now defunt or fixed. …
- 9:57 PM Ticket #58 (Hangs during shutdown) created by
- Sometimes observed. Repeatable test case needed (but may be …
- 9:54 PM Ticket #57 (Symbol table editor problems: doesn't report correct status, apply is ...) created by
- * Symbol table editor sometimes doesn't display right, sometimes …
- 9:51 PM Ticket #56 (PGActions do not always clear their status (report "someone else owns ...) created by
- Sometimes buttons have no action because of prover-ownership being …
- 9:46 PM Ticket #55 (Parsing whole file is costly; lazy "gathering" parser strategy is flawed) created by
- Currently, parsing parses the entire file, but this is annoying for …
- 9:39 PM Ticket #54 (Support file operations save-as, rename, revert properly during script ...) created by
- These file operations corrupt the synchronisation with the prover: * …
- 9:32 PM Ticket #53 (Re-implement toolbar button enablers) created by
- Toolbar button enablers were previously implemented but very …
- 4:59 PM Ticket #52 (An issue with current version of Trac) created by
- Some things to be careful of when using this Trac: On editing a …
- 4:23 PM Ticket #51 (Add processing direction to 'active script' decorator) created by
- Currently, Proof Script Document decorators display if a script is …
- 1:12 PM Ticket #28 (Newlines in PGIP console are lost) closed by
- worksforme: Tried this again, seems fine now!
- 1:08 PM Ticket #50 (Make sure PG perspective is default on product startup.) closed by
- fixed
Jan 30, 2007:
- 5:51 PM Ticket #50 (Make sure PG perspective is default on product startup.) created by
- Recently broken, the resource perspective appears to be default at the …
- 5:47 PM Ticket #49 (Make sure File->Open produces sensible feedback when attempted with ...) created by
- At the moment
File->Openproduces a confusingly blank canvas or … - 5:42 PM Ticket #48 (Support editing proof script files outside workspace) closed by
- wontfix
- 5:41 PM Ticket #48 (Support editing proof script files outside workspace) created by
- It seems desirable to support editing files outside workspace. To do …
- 5:36 PM Ticket #47 (Complete configuration of <lexicalsyntax> elements) created by
- Lexical syntax elements allow correct and dynamically extensible …
- 5:33 PM Ticket #46 (Extra view for Problem Details) created by
- Extra view for "Problem Details" in case of prover error, to get …
- 5:30 PM Ticket #45 (Use workbench progress feedbacks; provide busy indications) created by
- We should use workbench progress feedback for proof (not so important: …
- 5:28 PM Ticket #44 (Support openblock/closeblock elements in prover parse output.) created by
- The openblock/closeblock elements should allow us to remove Isabelle …
- 5:22 PM Ticket #43 (Improve output markup (pgml.xsl)) created by
- Output markup can and should be improved a lot by extending the XSL …
- 5:17 PM Ticket #42 (Extract Isabelle-specific behaviour; design prover extension point) created by
- We should extract the Isabelle specific behaviour of the current …
- 5:08 PM Ticket #41 (Revive GEF dependency graph viewer as a separate plugin) created by
- Elina Timiriassova contributed a GEF-based dependency graph viewer as …
- 5:04 PM Ticket #40 (Implement document regions and annotations/markers for colouring) created by
- Use markers or annotations instead of coloured tokens. Fixes lots of …
- 4:59 PM Ticket #39 (Code cleanups: use tag CLEANUP for old code prior to removal) created by
- To avoid deleting useful old code, or removing it before new code is …
- 4:56 PM Ticket #38 (Add automated testing framework) created by
- This is desperately wanted. We need a testing framework which …
- 4:52 PM Ticket #37 (ProverKnowledge updates and improvements) created by
- Various desirable improvements: * Fix output conversion from XML …
- 4:43 PM Ticket #36 (Split stream for console into input/output and give input a different ...) created by
- A minor improvement for the PGIP console is to display input/output in …
- 4:41 PM Ticket #35 (Implement Java PGIP abstraction, independently of Eclipse code) created by
- We should have a PGIP abstraction in Java which is used to represent …
- 4:37 PM Ticket #34 (Event processing cleanups) created by
- Event model needs cleanup/simplification to be more efficient. * …
- 4:35 PM Ticket #33 (Fix interrupts: interrupt crashes prover and interrupt ineffective) created by
- 1. interrupt can cause prover crash (why?) 2. interrupt has hardwired …
- 4:32 PM Ticket #32 (Add some user documentation) created by
- We need some user-level documentation to include in the product. It …
- 4:28 PM Ticket #31 (Decorators not always updated) created by
- There are some cases when the decorators do not get updated to reflect …
- 4:27 PM Ticket #30 (Outline view should update after any parse) created by
- There are some cases when the outline view does not get updated. …
- 4:23 PM Ticket #29 (Symbol table editing scheme: fix filename and add edit action rather ...) created by
- We're moving to having a fixed
.default.symsymbol table associated … - 4:19 PM Ticket #28 (Newlines in PGIP console are lost) created by
- Newlines in PGIP console (e.g. in parseresult) are lost. Hopefully …
- 4:08 PM Ticket #27 (Efficiency problems with larger files and larger outputs) created by
- Try processing BigTheory?.thy and compare time taken in Eclipse with …
- 4:02 PM Ticket #26 (Investigate and fix small-scale efficiency problems (e.g. undo in ...) created by
- Undo is very slow when a bunch of commands are to be undone, it can be …
- 3:57 PM Ticket #25 (Review in-code TODO and FIXME tasks) created by
- Review all the in-code tasks generated by TODO and FIXME, currently …
- 3:49 PM Ticket #24 (Replace current undo management with document-based undo mechanism) created by
- The current undo management code uses a long history of commands sent …
- 3:42 PM Ticket #23 (Test and refine capabilities/activities) created by
- The plugin.xml file adds some support for capabilities which can be …
- 3:38 PM Ticket #22 (Refactor SessionManager) created by
- Continue refactoring of SessionManager to clean up responsibilities …
- 3:32 PM Ticket #21 (Refactor to remove DummyDocElement) created by
- Refactor to remove the DummyDocElement atrocity. We should remove …
- 3:29 PM Ticket #20 (Fix ProofScriptEditor to change symbols cleanly) created by
- ProofScriptEditor should change symbols cleanly, ideally without …
- 3:28 PM Ticket #19 (Use markers/positions for document processed and locked offsets) created by
- Instead of using fixed offsets, the positions should move with edits …
- 3:26 PM Ticket #18 (Add hover for prover output (on any blue space)) created by
- To support document-based editing without displaying intermittent …
- 3:24 PM Ticket #17 (Add clear button for prover output) created by
- Add clear button for prover output, which clears history.
- 3:23 PM Ticket #16 (Move cursor and scroll during do/undo) created by
- Restore cursor movement behaviour.
- 1:11 PM Ticket #15 (Concurrency fixes in GetCommandResponseAction) created by
- Uses double checked locking and a static field.
- 1:10 PM Ticket #14 (Concurrency fixes) created by
- Thread safety in the code needs to be carefully reviewed. …
- 12:19 PM Ticket #13 (Add proof object search facilities to IdView) created by
- Add a proof object search facility to IdView, similar to the Open …
- 12:06 PM Ticket #12 (Polish Proof Objects View; Link to Prover Knowledge) created by
- Proof Objects view needs some polish: 1. Glitch when editing theory …
Jan 29, 2007:
- 2:27 PM Ticket #11 (Builder for parsing/proving files automatically) created by
- Add builder for parsing/proving files automatically. This is partly …
- 2:23 PM Ticket #10 (Refactor and enhance document model) created by
- Refactor ProofScriptDocument to remove the document model explicitly …
- 2:21 PM Ticket #9 (Fix history in output view) created by
- History in output view (or browsing it) is garbled.
- 2:19 PM Ticket #8 (Cleanup active script handling in actions) created by
- Active script switching needs overhaul. Switching should be managed …
- 2:17 PM Ticket #7 (Finish proof explorer: inherit decorators, menus, etc. from Project ...) created by
- The Proof Explorer view needs to inherit more of the functionality of …
- 2:15 PM Ticket #6 (Add code folding for proof scripts) created by
- Add code folding for proof scripts. Hua Yang had some experimental …
- 12:25 PM Ticket #5 (Replace ThreadPool with Eclipse job management) created by
- We should replace our ThreadPool? code with the core Eclipse job …
Jan 26, 2007:
- 9:22 PM Ticket #4 (Use stixfonts once they become available) created by
- See http://www.stixfonts.com - Is it possible to redistribute them …
- 7:59 PM Ticket #3 (Improve code quality: address J2SE best practices in TPTP analysis) created by
Jan 22, 2007:
Note: See TracTimeline
for information about the timeline view.
