Custom Query (361 matches)
Results (49 - 51 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #48 | wontfix | Support editing proof script files outside workspace | ||
| Description |
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. |
|||
| #74 | wontfix | Coq: bug in electric terminator: typing '.' in comment causes comment to be sent and locked | ||
| Description |
When I type a '.' within a comment, the comment is sent to Coq and then locked. This is obviously not what I want! A '.' within a comment should be ignored. Emacs : GNU Emacs 22.0.93.1 (x86_64-redhat-linux-gnu, GTK+ Version 2.10.9)
Package: Proof General current state: ============== (setq
|
|||
| #118 | wontfix | Complete X-Symbol unicode patch and add symbol configuration for Isabelle | ||
| Description |
X-Symbol unicode patch allows use of token languages to input Unicode characters. Early work on this is now included in Proof General's bundled version of X-Symbol. |
|||
