{5} Assigned, Active Tickets by Owner (Full Description) (13 matches)
List tickets assigned, group by ticket owner. This report demonstrates the use of full-row display.
David Aspinall (8 matches)
Ticket | Summary | Component | Milestone | Type | Created | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#250 | Interrupt causes document inconsistency | 1:pg-eclipse | defect | Sep 5, 2008 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Test: process AThousandTheorems and interrupt. This problem is introduced by the simplification of the event structure and queue management. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#249 | Script management error for locales; undo action failure should not generate markers | 1:pg-eclipse | Sep 4, 2008 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Test case: undo in TestLocale?.thy from lemma line (inside locale) to theory line. This causes a "kill" command to be sent which gives the error: Illegal application of command "kill" in local theory mode At command "kill". Additionally, this attaches an error marker for the undo region to the code, which is quite confusing (because it appears in processed text) and also hard to get rid of (would be fixed if we removed error markers upon correct processing of commands, see #248). |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#127 | Fix Action Bar active editor switching; simplify actions | 1:pg-eclipse | defect | Jul 7, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
PG often loses track of the active editor. Instead of self managing this in our own way we should use the standard Eclipse mechanism for retargeted actions. It's slightly more complicated, but allows us to attach an action set to the script editor only and our own views. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#47 | Complete configuration of <lexicalsyntax> elements | 1:pg-eclipse | enhancement | Jan 30, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Lexical syntax elements allow correct and dynamically extensible keyword handling. Presently needs further work in Isabelle as well as Eclipse. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#134 | Generalise lexing to better match Isar syntax | 1:pg-eclipse | enhancement | Jul 19, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
We should generalise lexing to better match Isar's syntax rules. These are rather complex so we may be satisfied for now with an approximation (ultimately and unfortunately: prover-specific Java code to fine-tune). The PGIP lexicalstructure element can be tweaked to match. Tricky part here is allowing some update on-the-fly. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#169 | Complete buffer history enhancement | 2:pg-emacs | PG-Emacs-4.3 | enhancement | Dec 13, 2007 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The buffer history addition is not quite ready, so pulled from 3.7. The ring management needs some logic fixes, and the interface should be made compatible with XEmacs and enhanced to allow dynamic switch on/off and obey saved option. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#34 | Event processing cleanups | 1:pg-eclipse | task | Jan 30, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Event model needs cleanup/simplification to be more efficient.
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#22 | Refactor SessionManager | 1:pg-eclipse | enhancement | Jan 30, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Continue refactoring of SessionManager to clean up responsibilities and add access controls on underlying models of prover state, etc. Queue handling, prover info and state, etc, should be handled as delegated behaviour (see treatment of ControlledDocuments). |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Graham Dutton (4 matches) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Ticket | Summary | Component | Milestone | Type | Created | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#240 | Bad behaviour in startup when proof executables (isabelle, isatool) not found | 1:pg-eclipse | defect | Aug 15, 2008 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
If the workbench is started when an editor on a script file is open, the user is shown the dialog for entering a path, but the system repeatedly tries the broken path. If the workbench is started without an open editor, it hangs when the first editor is opened. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#244 | Comical giant icons in outline view | 1:pg-eclipse | defect | Sep 1, 2008 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Sometimes the outline view displays abnormally large icons. Precise recipe for duplications is needed; maybe it only happens in remote X server cases? |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#13 | Add proof object search facilities to IdView | 1:pg-eclipse | enhancement | Jan 30, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Add a proof object search facility to IdView, similar to the Open Type dialog in Java, so we can find names dynamically. A more advanced facility would be to search on object contents. This may require using prover-side search, and/or interfacing with ProverKnowledge. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#43 | Improve output markup (pgml.xsl) | 1:pg-eclipse | enhancement | Jan 30, 2007 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Output markup can and should be improved a lot by extending the XSL file for PGML.
Longer term it is frustrating to have the input/output disparity so great. The HTML view may be better replaced with a StyledText once that is flexible enough and a semi-wysiwyg approach is possible. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
hendrik (1 match) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Ticket | Summary | Component | Milestone | Type | Created | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
#454 | coq mode: compile before import fails when no .v file | 2:pg-emacs | PG-Emacs-4.3 | enhancement | Oct 2, 2012 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Some users use .vo files without having the corresponding .v files. the compile before require feature should consider a .vo up-to-date if there is no corresponding .v file. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||