Custom Query (361 matches)

A minor improvement for the PGIP console is to display input/output in different colours or fonts.

This should be easy: message streams can have colour/fonts attached, so we just need to split PGIP stream into two.

It seems desirable to support editing files outside workspace.

To do this we need to adjust ProofScriptDocument to remove the resource field and possibly prover syntax field (which is not initialised when making documents by the Eclipse standard way).

A first attempt at this showed that it really is too difficult to do well. Viewing a script is possible but as soon as we do anything sophisticated with the document we need the extra support available for files which actually reside in the workspace. Especially markers, which we use extensively for state management and problems/tasks. Eclipse currently only allows them on resources. Managing two different kinds of documents (internal and external) gets very nasty in the code quite quickly.

This ticket is here as a reference for the issue and reminder of problems.

At the moment File->Open produces a confusingly blank canvas or exceptions.

Ideally we should display a dialogue or message in the incompletely-configured editor. Or maybe revert to the ordinary text editor, somehow.

This worked in a previous revision, but changes in document provider engagement have perhaps broken it.