Custom Query (361 matches)
Results (64 - 66 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #175 | fixed | ProofGeneral accidentally resets itself while scrolling | ||
| Description |
When using ProofGeneral with XEmacs 21.4 and the CVS version of Isabelle, the following problem occurs: when stepping through a theory file using the "Next" button, ProofGeneral sometimes accidentaly resets itself when the cursor hits the bottom of the window in which the theory file is displayed, and XEmacs tries to scroll the text in the window. The effect of this bug is that the part of the theory file that was already processed is no longer coloured blue, and ProofGeneral's internal pointer indicating the next command to be processed is reset to the beginning of the theory file, causing the Isabelle process and ProofGeneral to get completely out of sync. In addition, the error message "(1) (error/warning) Error in 'post-command-hook' (setting hook to nil): (error Lisp nesting exceeds 'max-lisp-eval-depth')" is displayed. This problem does not occur with XEmacs 21.5, though. |
|||
| #176 | fixed | Allow isabelle-chosen-logic to be set by variable comment in thy file | ||
| Description |
At the moment a comment like (* -*- isabelle-chosen-logic: "HOL-Nominal" -*- *) doesn't work as desired because of the way the program arguments are set only when we change with the menu. Could improve this by using a calculate function like Coq does. |
|||
| #177 | fixed | Complete Unicode Token coding system and input method | ||
| Description |
This is an experimental partial replacement for X-Symbol. Ultimately it should be possible to extend it to handle control characters for subscript/superscript and other highlights. What is missing at the moment is a coding system. The (efficient) way to do this requires writing decode/encode functions in the dedicated CCL language, maybe. Another possibility might be to use a decode map in quail, but examples/documentation are thin on the ground. |
|||
