Custom Query (361 matches)
Results (79 - 81 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #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. |
|||
| #178 | worksforme | Emacs occasionally hangs when doing isearch-forward. | ||
| Description |
Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor occasionally hangs when doing isearch-forward. E.g. reproduce this by visiting Isabelle/src/HOL/Lambda/WeakNorm.thy: type C-s, type "c" "o" "n" "s" (which finds an occurreny of "Cons" in the text), continuing to type "t" makes emacs hang; after C-g it works again, but there is some danger it will again hang later. |
|||
