{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.

  • Re-engage Ahsan's PGIP-filter in SessionManager.
  • Consider separating internally generated events (!ScriptingUIEvents) from PGIP events generated by incoming prover messages. Incoming prover messages can be fast and furious, and shouldn't be sent around to every control under the sun.
#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.

  • More x-symbol compatibility to support Isabelle symbol usage may be possible (e.g., superscripts/subscripts).
  • Can we make some parameters which can be configured in the interface to set fonts/colours, etc?

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.

Note: See TracReports for help on using and creating reports.